IsaMorph is a live CD for GNU/Linux, which uses Morphix as a base and includes Isabelle, an interactive theorem prover.
IsaMorph is a Linux distribution Live CD that comes with the interactive theorem prover Isabelle. With IsaMorph, you can get a fully functional theorem proving environment without having to install GNU/Linux or Isabelle. Simply insert the CD into your PC and in just five minutes, you can prove your first theorem. All the programs distributed within IsaMorph are free software, which means that you can freely copy, modify and distribute the operating system and the applications contained in the CD.
To get started, insert the CD into your Intel-compatible PC or laptop and reboot the computer. Ensure that the first boot device is CD, and if you're unsure about how to do this, get help from your system administrator or someone who knows how to do it. As your computer boots up, it will automatically search for the CD in the drive. After some time, a menu will appear, and you can press the Enter key or wait for some time to continue booting from the CD.
IsaMorph comes with a fully working Isabelle environment that supports proving and document generation. This includes Isabelle 2005, the interactive theorem prover with at least the following logics compiled in: HOL, HOL-Complex, ZF, FOL, and Pure. You can immediately start proving theorems in any of these logics after booting IsaMorph. The CD also contains an offline version of Isabelle's tutorials and theory documentation.
In addition to Isabelle, IsaMorph also includes other useful applications for common use, such as a user-friendly desktop (Gnome), an internet browser (Mozilla), and more. The CD includes a powerful user interface for Isabelle called Proof General, which is built with GNU Emacs (version 22.0.50), the editor that also serves as the main user interface for Isabelle. It also comes with the Standard ML Environment, SML of New Jersey (version 110.56), which is used for compiling and executing Isabelle, and a complete LaTeX environment called teTeX (version 2.0.2) for the generation of proof documents.
This release of IsaMorph updates all software on the CD, including all base utilities and all Isabelle-related software. This is also the first release featuring the latest Isabelle version (2005), X-Symbol (3.6pre), and HOL-TestGen (1.1.1). Overall, if you're looking for a user-friendly and comprehensive theorem proving environment with all the necessary applications, tools, and document generators, IsaMorph is definitely worth a try.
To get started, insert the CD into your Intel-compatible PC or laptop and reboot the computer. Ensure that the first boot device is CD, and if you're unsure about how to do this, get help from your system administrator or someone who knows how to do it. As your computer boots up, it will automatically search for the CD in the drive. After some time, a menu will appear, and you can press the Enter key or wait for some time to continue booting from the CD.
IsaMorph comes with a fully working Isabelle environment that supports proving and document generation. This includes Isabelle 2005, the interactive theorem prover with at least the following logics compiled in: HOL, HOL-Complex, ZF, FOL, and Pure. You can immediately start proving theorems in any of these logics after booting IsaMorph. The CD also contains an offline version of Isabelle's tutorials and theory documentation.
In addition to Isabelle, IsaMorph also includes other useful applications for common use, such as a user-friendly desktop (Gnome), an internet browser (Mozilla), and more. The CD includes a powerful user interface for Isabelle called Proof General, which is built with GNU Emacs (version 22.0.50), the editor that also serves as the main user interface for Isabelle. It also comes with the Standard ML Environment, SML of New Jersey (version 110.56), which is used for compiling and executing Isabelle, and a complete LaTeX environment called teTeX (version 2.0.2) for the generation of proof documents.
This release of IsaMorph updates all software on the CD, including all base utilities and all Isabelle-related software. This is also the first release featuring the latest Isabelle version (2005), X-Symbol (3.6pre), and HOL-TestGen (1.1.1). Overall, if you're looking for a user-friendly and comprehensive theorem proving environment with all the necessary applications, tools, and document generators, IsaMorph is definitely worth a try.
What's New
Version 0.9: N/A