src/HOL/README.html
author paulson
Fri, 29 Nov 1996 18:03:21 +0100
changeset 2284 80ebd1a213fd
parent 2080 12eed4cec935
child 3125 3f0ab2c306f7
permissions -rw-r--r--
Swapped arguments of Crypt (for clarity and because it is conventional)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
     1
<!-- $Id$ -->
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     2
<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     3
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     4
<H2>HOL: Higher-Order Logic with curried functions</H2>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     5
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     6
This directory contains the Standard ML sources of the Isabelle system for
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     7
Higher-Order Logic with curried functions.  Important files include
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     8
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
     9
<DL>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    10
<DT>ROOT.ML
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    11
<DD>loads all source files.  Enter an ML image containing Pure
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    12
Isabelle and type: use "ROOT.ML";<P>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    13
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    14
<DT>Makefile
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    15
<DD>compiles the files under Poly/ML or SML of New Jersey<P>
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    16
</DL>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    17
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    18
<P>There are several subdirectories.  To execute them, issue the command
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    19
<PRE>
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    20
        use_dir "<I>&lt;DIR&gt;</I>";
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    21
</PRE>
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    22
where <I>&lt;DIR&gt;</I> is the desired directory 
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    23
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    24
<DL>
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    25
<DT>ex
2080
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    26
<DD>general examples
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    27
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    28
<DT>Auth
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    29
<DD>a new approach to verifying authentication protocols 
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    30
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    31
<DT>IMP
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    32
<DD>mechanization of a large part of a semantics text by Glynn Winskel
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    33
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    34
<DT>Integ
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    35
<DD>a theory of the integers including efficient integer calculations
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    36
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    37
<DT>IOA
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    38
<DD>extended example of Input/Output Automata (takes a long time to run!)
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    39
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    40
<DT>Lambda
12eed4cec935 Fuller description of examples
paulson
parents: 1341
diff changeset
    41
<DD>a proof of the Church-Rosser theorem for lambda-calculus
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    42
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    43
<DT>Subst
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    44
<DD>subdirectory defining a theory of substitution and unification.
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    45
</DL>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    46
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    47
Useful references on Higher-Order Logic:
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    48
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    49
<UL>
1341
69fec018854c HTML version of README
clasohm
parents: 1339
diff changeset
    50
<LI>P. B. Andrews,<BR>
69fec018854c HTML version of README
clasohm
parents: 1339
diff changeset
    51
    An Introduction to Mathematical Logic and Type Theory<BR>
69fec018854c HTML version of README
clasohm
parents: 1339
diff changeset
    52
    (Academic Press, 1986).
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    53
1341
69fec018854c HTML version of README
clasohm
parents: 1339
diff changeset
    54
<LI>J. Lambek and P. J. Scott,<BR>
69fec018854c HTML version of README
clasohm
parents: 1339
diff changeset
    55
    Introduction to Higher Order Categorical Logic (CUP, 1986)
1339
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    56
</UL>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    57
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL"
clasohm
parents:
diff changeset
    58
</BODY></HTML>