src/CTT/README.html
changeset 3279 815ef5848324
parent 1341 69fec018854c
child 15283 f21466450330
     1.1 --- a/src/CTT/README.html	Wed May 21 17:11:46 1997 +0200
     1.2 +++ b/src/CTT/README.html	Wed May 21 17:13:00 1997 +0200
     1.3 @@ -1,23 +1,12 @@
     1.4 -<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
     1.7  
     1.8  <H2>CTT: Constructive Type Theory</H2>
     1.9  
    1.10 -This directory contains the Standard ML sources of the Isabelle system for
    1.11 -Constructive Type Theory (extensional equality, no universes).  Important
    1.12 -files include
    1.13 +This directory contains the ML sources of the Isabelle system for
    1.14 +Constructive Type Theory (extensional equality, no universes).<p>
    1.15  
    1.16 -<DL>
    1.17 -<DT>ROOT.ML
    1.18 -<DD>loads all source files.  Enter an ML image containing Pure
    1.19 -Isabelle and type: use "ROOT.ML";<P>
    1.20 -
    1.21 -<DT>Makefile
    1.22 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    1.23 -
    1.24 -<DT>ex
    1.25 -<DD>subdirectory containing examples.  To execute them, enter an ML image
    1.26 -containing CTT and type: use "ex/ROOT.ML";<P>
    1.27 -</DL>
    1.28 +The <tt>ex</tt> subdirectory contains some examples.<p>
    1.29  
    1.30  Useful references on Constructive Type Theory:
    1.31  
    1.32 @@ -29,4 +18,6 @@
    1.33  <LI>	Simon Thompson,<BR>
    1.34  	Type Theory and Functional Programming (Addison-Wesley, 1991)
    1.35  </UL>
    1.36 -</BODY></HTML>
    1.37 +
    1.38 +</BODY>
    1.39 +</HTML>