--- a/src/HOL/README.html Wed May 21 17:11:46 1997 +0200
+++ b/src/HOL/README.html Wed May 21 17:13:00 1997 +0200
@@ -1,26 +1,12 @@
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
-<H2>HOL: Higher-Order Logic with curried functions</H2>
-
-This directory contains the Standard ML sources of the Isabelle system for
-Higher-Order Logic with curried functions. Important files include
+<H2>HOL: Higher-Order Logic</H2>
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";<P>
+This directory contains the ML sources of the Isabelle system for
+Higher-Order Logic.<P>
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
-</DL>
-
-<P>There are several subdirectories. To execute them, issue the command
-<PRE>
- use_dir "<I><DIR></I>";
-</PRE>
-where <I><DIR></I> is the desired directory
-
+There are several subdirectories with examples:
<DL>
<DT>ex
<DD>general examples