src/HOL/README.html
changeset 3279 815ef5848324
parent 3125 3f0ab2c306f7
child 4622 85aae356570c
     1.1 --- a/src/HOL/README.html	Wed May 21 17:11:46 1997 +0200
     1.2 +++ b/src/HOL/README.html	Wed May 21 17:13:00 1997 +0200
     1.3 @@ -1,26 +1,12 @@
     1.4  <!-- $Id$ -->
     1.5 -<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
     1.6 +<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
     1.7  
     1.8 -<H2>HOL: Higher-Order Logic with curried functions</H2>
     1.9 -
    1.10 -This directory contains the Standard ML sources of the Isabelle system for
    1.11 -Higher-Order Logic with curried functions.  Important files include
    1.12 +<H2>HOL: Higher-Order Logic</H2>
    1.13  
    1.14 -<DL>
    1.15 -<DT>ROOT.ML
    1.16 -<DD>loads all source files.  Enter an ML image containing Pure
    1.17 -Isabelle and type: use "ROOT.ML";<P>
    1.18 +This directory contains the ML sources of the Isabelle system for
    1.19 +Higher-Order Logic.<P>
    1.20  
    1.21 -<DT>Makefile
    1.22 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    1.23 -</DL>
    1.24 -
    1.25 -<P>There are several subdirectories.  To execute them, issue the command
    1.26 -<PRE>
    1.27 -        use_dir "<I>&lt;DIR&gt;</I>";
    1.28 -</PRE>
    1.29 -where <I>&lt;DIR&gt;</I> is the desired directory 
    1.30 -
    1.31 +There are several subdirectories with examples:
    1.32  <DL>
    1.33  <DT>ex
    1.34  <DD>general examples