src/LCF/README.html
author clasohm
Fri, 17 Nov 1995 13:22:50 +0100
changeset 1341 69fec018854c
child 3279 815ef5848324
permissions -rw-r--r--
HTML version of README
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     1
<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     2
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     3
<H2>LCF: Logic for Computable Functions</H2>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     4
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     5
This directory contains the Standard ML sources of the Isabelle system for
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     6
LCF.  It is loaded upon FOL, not Pure Isabelle.  Important files include
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     7
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     8
<DL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     9
<DT>ROOT.ML
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    10
<DD>loads all source files.  Enter an ML image containing FOL
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    11
Isabelle and type: use "ROOT.ML";<P>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    12
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    13
<DT>Makefile
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    14
<DD>compiles the files under Poly/ML or SML of New Jersey<P>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    15
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    16
<DT>ex.ML
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    17
<DD>file containing examples.  To execute it, enter an ML image
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
containing LCF and type:    use "ex.ML";
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    19
</DL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    20
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    21
Useful references on First-Order Logic:
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    22
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    23
<UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    24
<LI>Lawrence C. Paulson,<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    25
    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    26
</UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    27
</BODY></HTML>