diff -r b571d997178d -r 6cb6dd05d761 README
--- a/README	Tue Jul 12 18:30:53 1994 +0200
+++ b/README	Tue Jul 12 18:38:39 1994 +0200
@@ -25,11 +25,12 @@
 using the Bourne shell, sh.
 
 ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
-images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
-starting with "/").
+images.  This directory *must* be different from the Isabelle source
+directory.  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
-required for New Jersey ML).
+ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
+required for New Jersey ML.
 
 ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
 ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
@@ -52,6 +53,7 @@
   make-all-poly		sample make-all invocation for Poly/ML
   make-all-nj		sample make-all invocation for SML of NJ
   change_simp		shell script to help convert sources to new simplifier
+  conv-theory-files.pl  perl script to rename old theory files
   expandshort		shell script to expand "shortcuts" in files
   prove_goal.el       	Emacs command to change proof format
   xlisten		shell script for running Isabelle under X
@@ -125,4 +127,4 @@
 D-80290 Muenchen
 Germany
 
-Last updated 13 May 1994
+Last updated 20 May 1994