# HG changeset patch # User lcp # Date 755805003 -3600 # Node ID 7646f5b4653c8cb7b8c03e9fc1c169a0a32420b9 # Parent 1315ce07f5156e941d89e236bdd327b2ade82005 added isabelle-users paragraph diff -r 1315ce07f515 -r 7646f5b4653c README --- a/README Mon Dec 13 18:48:47 1993 +0100 +++ b/README Mon Dec 13 18:50:03 1993 +0100 @@ -16,7 +16,7 @@ 2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or later). Poly/ML is a commercial product and costs money, but it is reliable and its database system is convenient for interactive -work. SML of New Jersey requires lots of memory and disc space, but it is +work. SML of New Jersey requires lots of store and disc space, but it is free and its code sometimes runs faster. Both compilers are perfectly satisfactory for running Isabelle. @@ -27,7 +27,7 @@ images. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one starting with "/"). -ML_DBASE is an absolute pathname to the initial Poly/ML database (not +ML_DBASE is an *absolute* pathname to the initial Poly/ML database (not required for New Jersey ML). ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml". If @@ -79,7 +79,7 @@ good way to get started. Each object-logic is built on top of Pure Isabelle, and possibly on top of -another object logic (like FOL or LK). A database or binary called Pure is +another object logic like FOL or LK. A database or binary called Pure is first created, then the object-logic is loaded on top. Poly/ML extends Pure using its "make_database" operation. Standard ML of New Jersey starts with the Pure core image and loads the object-logic's ROOT.ML. @@ -98,6 +98,12 @@ ------------------------------------------------------------------------------ +The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum +for Isabelle users to discuss problems and exchange information. To join, +send a message to isabelle-users-request@cl.cam.ac.uk. + +------------------------------------------------------------------------------ + Please report any problems you encounter. While we shall try to be helpful, we can accept no responsibility for the deficiences of Isabelle and their consequences. @@ -115,4 +121,4 @@ D-80290 Muenchen Germany -Last updated 5 November 1993 +Last updated 13 December 1993