[Morphix-user] First public relase of IsaMorph, a Linux live CD featuring Isabelle 2004

[Achim D. B. <br...@sp...>]

I'm happy to announce the first public version of


                 IsaMorph, version 0.1.0. 
         http://www.brucker.ch/projects/isamorph/

IsaMorph is a GNU/Linux 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
prove your first theorem within minutes.

IsaMorph contains a fully working Isabelle environment supporting proving 
and document generation, this includes:

- Isabelle (version 2004), see http://isabelle.in.tum.de
  The interactive theorem prover Isabelle 2004 with at least the
  following logics compiled in: Pure, FOL, Sequents, ZF, HOL, HOLCF, 
  and HOL-Complex.
  Thus, after booting IsaMorph you can immediately prove theorems in 
  any of these logics. The CD includes a offline version of the Isabelle
  tutorials and theory documentation.

- Proof General (version 3.4) together with X-Symbol support
  A powerful User Interface for 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.
 

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.


You can download the iso-image from:
         http://www.brucker.ch/projects/isamorph/



Hope you enoy using it and looking forward to your feedback.

Achim