added isabelle-users paragraph
authorlcp
Mon, 13 Dec 1993 18:50:03 +0100
changeset 1967646f5b4653c
parent 195 1315ce07f515
child 197 7c7179e687b2
added isabelle-users paragraph
README
     1.1 --- a/README	Mon Dec 13 18:48:47 1993 +0100
     1.2 +++ b/README	Mon Dec 13 18:50:03 1993 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
     1.5  (Version 0.93 or later).  Poly/ML is a commercial product and costs money,
     1.6  but it is reliable and its database system is convenient for interactive
     1.7 -work.  SML of New Jersey requires lots of memory and disc space, but it is
     1.8 +work.  SML of New Jersey requires lots of store and disc space, but it is
     1.9  free and its code sometimes runs faster.  Both compilers are perfectly
    1.10  satisfactory for running Isabelle.
    1.11  
    1.12 @@ -27,7 +27,7 @@
    1.13  images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
    1.14  starting with "/").
    1.15  
    1.16 -ML_DBASE is an absolute pathname to the initial Poly/ML database (not
    1.17 +ML_DBASE is an *absolute* pathname to the initial Poly/ML database (not
    1.18  required for New Jersey ML).
    1.19  
    1.20  ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
    1.21 @@ -79,7 +79,7 @@
    1.22  good way to get started.
    1.23  
    1.24  Each object-logic is built on top of Pure Isabelle, and possibly on top of
    1.25 -another object logic (like FOL or LK).  A database or binary called Pure is
    1.26 +another object logic like FOL or LK.  A database or binary called Pure is
    1.27  first created, then the object-logic is loaded on top.  Poly/ML extends
    1.28  Pure using its "make_database" operation.  Standard ML of New Jersey starts
    1.29  with the Pure core image and loads the object-logic's ROOT.ML.
    1.30 @@ -98,6 +98,12 @@
    1.31  
    1.32  ------------------------------------------------------------------------------
    1.33  
    1.34 +The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum
    1.35 +for Isabelle users to discuss problems and exchange information.  To join,
    1.36 +send a message to isabelle-users-request@cl.cam.ac.uk.
    1.37 +
    1.38 +------------------------------------------------------------------------------
    1.39 +
    1.40  Please report any problems you encounter.  While we shall try to be helpful,
    1.41  we can accept no responsibility for the deficiences of Isabelle and their
    1.42  consequences.
    1.43 @@ -115,4 +121,4 @@
    1.44  D-80290 Muenchen
    1.45  Germany
    1.46  
    1.47 -Last updated 5 November 1993
    1.48 +Last updated 13 December 1993