Further work

Areas that need further development include:

• Methods for entering specifications of theorems.
  The current interface requires the user to type in the theorem in a language specific to Isabelle [example]. If would be nice if we could make use of an equation editor such as Jex, an open source equation editor written in Java that outputs MathML or Latex formatted equations. Even better would be something like the Freehand Formula Entry System.
• More complete PGIP support, and porting PGIP to other proof assistants.
  
• Online help/documentation.
• Theory revision control.
  It would be good to allow users to save revisions of the theories they are developing. Subversion is an open source version control library that aims to do better where CVS is clunky. It runs on Unix, Win32, BeOS, OS/2 and MacOS X.
• Server rewrite.
  The Isabelle Server module should be rewritten to work like a traditional login system- once authenticated the proof engine should run as the user that has just logged in.
• Ports to other platforms.
  Igloo has only been tested on one platform (Debian GNU/Linux). It should not be too hard to get it running on other platforms, but this has not yet been attempted.