README
changeset 609 6d520505e704
parent 470 6cb6dd05d761
child 816 2f89be458be5
equal deleted inserted replaced
608:245633e2fd57 609:6d520505e704
     1 		     ISABELLE-93 DISTRIBUTION DIRECTORY
     1 		     ISABELLE-94 DISTRIBUTION DIRECTORY
     2 
     2 
     3 ------------------------------------------------------------------------------
     3 ------------------------------------------------------------------------------
     4 ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     4 ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     5 DOCUMENTATION.
     5 DOCUMENTATION.  
       
     6 
       
     7 In particular, theory files are no longer forced into lower case, but must
       
     8 be identical to the actual theory name.  The command
       
     9 	conv-theory-files.pl | grep mv
       
    10 generates commands to rename all theory files in a directory hierarchy.  
     6 ------------------------------------------------------------------------------
    11 ------------------------------------------------------------------------------
     7 
    12 
     8 This directory contains the complete Isabelle system.  To build and test the
    13 This directory contains the complete Isabelle system.  To build and test the
     9 entire system, including all object-logics, use the shell script make-all.
    14 entire system, including all object-logics, use the shell script make-all.
    10 Pure Isabelle and each of the object-logics can be built separately using the
    15 Pure Isabelle and each of the object-logics can be built separately using the
    59   xlisten		shell script for running Isabelle under X
    64   xlisten		shell script for running Isabelle under X
    60   teeinput		shell script to run Isabelle, logging inputs to a file
    65   teeinput		shell script to run Isabelle, logging inputs to a file
    61   Pure			directory of source files for Pure Isabelle
    66   Pure			directory of source files for Pure Isabelle
    62   Provers		directory of generic theorem provers
    67   Provers		directory of generic theorem provers
    63 
    68 
    64 xlisten sets up a window running Isabelle, with a separate small "listener"
    69 David Aspinall has written a user interface for Isabelle.  It runs under
    65 window, which keeps a log of all input lines.  This log is a useful record
    70 GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
    66 of a session.  If you are not running X windows, teeinput can still be used at
    71 from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
    67 least to record (if not to display) the log.
    72 
       
    73 A *very* primitive alternative, xlisten sets up a window running Isabelle,
       
    74 with a separate small "listener" window, which keeps a log of all input
       
    75 lines.  If you are not running the X Window System, teeinput can still be
       
    76 used to record the log.
    68 
    77 
    69 The following subdirectories contain object-logics:
    78 The following subdirectories contain object-logics:
    70   FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    79   FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    71   FOLP 	  First-Order Logic with Proof terms
    80   FOLP 	  First-Order Logic with Proof terms
    72   ZF	  Zermelo-Fraenkel set theory
    81   ZF	  Zermelo-Fraenkel set theory
   120 Pembroke Street 
   129 Pembroke Street 
   121 Cambridge CB2 3QG 
   130 Cambridge CB2 3QG 
   122 England
   131 England
   123 
   132 
   124 Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   133 Tobias Nipkow			E-mail: nipkow@informatik.tu-muenchen.de
   125 Institut fuer Informatik	Phone: +49-89-2105-2690
   134 Institut für Informatik		Phone: +49-89-2105-2690
   126 T. U. Muenchen			Fax:   +49-89-2105-8183
   135 T. U. München			Fax:   +49-89-2105-8183
   127 D-80290 Muenchen
   136 D-80290 München
   128 Germany
   137 Germany
   129 
   138 
   130 Last updated 20 May 1994
   139 $Id$