IsaMorph is a linux distribution Live CD (based on Morphix) featuring the interactive theorem prover Isabelle. This means, you can boot from the CD and get a fully operational "theorem proving" environment without installing GNU/Linux or Isabelle. Just insert the CD in your PC and have five minutes later your first theorem proven. All programs distributed within IsaMorph are free software. This means that the operating system and the applications contained in this CD can be freely copied, modified and distributed. So please feel free to give copies to your friends or colleagues. Insert the CD into the CD drive on an Intel compatible PC or laptop. Now reboot the computer. Ensure that the first boot device is CD. For this, you may have to change the BIOS settings of your computer. If you are not familiar with it, get help from your system administrator or someone who knows how to do it. As the computer starts booting, it will search for a CD in the drive. A menu will appear after some time. Just press the Enter key or wait for some time. The computer will continue to boot from the CD and, hopefully, give you a graphical screen similar to what you are familiar with. You can click on the menu at the top left and start applications. IsaMorph contains a fully working Isabelle environment supporting proving and document generation, this includes: Isabelle (version 2005) The interactive theorem prover Isabelle 2005 with at least the following logics compiled in: HOL, HOL-Complex, ZF, FOL, and Pure. Thus, after booting IsaMorph you can immediately prove theorems in any of these logics. The CD includes a offline version of Isabelles tutorials and theory documentation. HOL-TestGen (version 1.1.1) A test case generator for specification based unit testing. It is built on top of the specfication and theorem proving environment Isabelle/HOL. Proof General (version 3.6pre) A powerful User Interface for Isabelle. SML of New Jersey (version 110.56) The Standard ML Environment used for compiling and executing Isabelle. GNU Emacs (version 22.0.50) The GNU Emacs editor which builds together with Proof General the main user interface of Isabelle. teTeX (version 2.0.2) A complete LaTeX environment used for the generation of proof documents. Other Applications In addition, the CD also contains a variety of applications for a common use. It includes a user-friendly desktop (Gnome) an Internet browser (Mozilla), and so on. Just take a look at the menu to find out many more. I tried to minimize the number of non Isabelle specific software to minimize the download size. Whats New in This Release: · This is release updates all software on the CD, including all base utilities and all Isabelle related software. · Particularly, this is the first release featuring the latest Isabelle version (2005), X-Symbol (3.6pre), and also HOL-TestGen (1.1.1)..

Isamorph - Gnu - Hol - Linux Live Cd - Theorem Prover - Live Cd - Based On - Isabelle - Theorem - Prover - Featuring - Interactive - Environment - Linux Distributions

Published By:Achim D. Brucker

License Type:Freeware

Date Added:22 October, 2010




Size:498.6 MB

Platform: Linux

What people say
- required fields
Related Downloads

GNU Gama is a package for adjustment of geodetic free networks (acronym Gama is formed from words geodesy and mapping).

DateSep 15, 2010

AuthorAles Cepek and Jan Pytel

Size614.4 KB




CategoryLinux Internet

ANDREWs Not a DVD Ripping and Encoding Wizard, but an interactive wrapper or a BASH script to simplify the use of OggEnc, MEncoder and mkv/ogmmerge to create, from a DVD, one or more Matroska or Ogg Media files containing an ISO/IEC  MPEG-4 Part

DateAug 27, 2010

AuthorAlessandro Di Rubbo

Size174.1 KB




CategoryLinux Multimedia

GNU Barcode is a tool to convert text strings to printed bars. GNU barcode supports a variety of standard codes to represent the textual strings and creates postscript output..

DateOct 16, 2010

AuthorAlessandro Rubini

Size327.7 KB




CategoryLinux Business

tarix is a simple indexer for POSIX and GNU tar files. The indexes allow fast extraction of files in the archive, especially on seekable tape devices.

DateSep 30, 2010


Size23.6 KB




CategoryLinux Utilities

GNU C library (glibc) is one of the most important components of GNU Hurd and most modern Linux distributions. GNU C library is used by almost all C programs and provides the most essential program interface.

DateOct 14, 2010

AuthorAndreas Jaeger

Size19.5 MB




CategoryLinux Programming