README
changeset 609 6d520505e704
parent 470 6cb6dd05d761
child 816 2f89be458be5
     1.1 --- a/README	Tue Sep 13 11:19:38 1994 +0200
     1.2 +++ b/README	Tue Sep 13 11:39:49 1994 +0200
     1.3 @@ -1,8 +1,13 @@
     1.4 -		     ISABELLE-93 DISTRIBUTION DIRECTORY
     1.5 +		     ISABELLE-94 DISTRIBUTION DIRECTORY
     1.6  
     1.7  ------------------------------------------------------------------------------
     1.8 -ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     1.9 -DOCUMENTATION.
    1.10 +ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
    1.11 +DOCUMENTATION.  
    1.12 +
    1.13 +In particular, theory files are no longer forced into lower case, but must
    1.14 +be identical to the actual theory name.  The command
    1.15 +	conv-theory-files.pl | grep mv
    1.16 +generates commands to rename all theory files in a directory hierarchy.  
    1.17  ------------------------------------------------------------------------------
    1.18  
    1.19  This directory contains the complete Isabelle system.  To build and test the
    1.20 @@ -61,10 +66,14 @@
    1.21    Pure			directory of source files for Pure Isabelle
    1.22    Provers		directory of generic theorem provers
    1.23  
    1.24 -xlisten sets up a window running Isabelle, with a separate small "listener"
    1.25 -window, which keeps a log of all input lines.  This log is a useful record
    1.26 -of a session.  If you are not running X windows, teeinput can still be used at
    1.27 -least to record (if not to display) the log.
    1.28 +David Aspinall has written a user interface for Isabelle.  It runs under
    1.29 +GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
    1.30 +from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
    1.31 +
    1.32 +A *very* primitive alternative, xlisten sets up a window running Isabelle,
    1.33 +with a separate small "listener" window, which keeps a log of all input
    1.34 +lines.  If you are not running the X Window System, teeinput can still be
    1.35 +used to record the log.
    1.36  
    1.37  The following subdirectories contain object-logics:
    1.38    FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    1.39 @@ -122,9 +131,9 @@
    1.40  England
    1.41  
    1.42  Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
    1.43 -Institut fuer Informatik	Phone: +49-89-2105-2690
    1.44 -T. U. Muenchen			Fax:   +49-89-2105-8183
    1.45 -D-80290 Muenchen
    1.46 +Institut für Informatik		Phone: +49-89-2105-2690
    1.47 +T. U. München			Fax:   +49-89-2105-8183
    1.48 +D-80290 München
    1.49  Germany
    1.50  
    1.51 -Last updated 20 May 1994
    1.52 +$Id$