The new interface to LEGO and other proof systems.
literate programming environment
search for definitions, proved lemmas, etc
generate time statistics for checking LEGO modules
CGI script which generates html pages from of a LEGO source file
The old interface to the LEGO machine