equal
deleted
inserted
replaced
|
1 LCF: Logic for Computable Functions |
|
2 |
|
3 This directory contains the Standard ML sources of the Isabelle system for |
|
4 LCF. It is loaded upon FOL, not Pure Isabelle. Important files include |
|
5 |
|
6 ROOT.ML -- loads all source files. Enter an ML image containing FOL and |
|
7 type: use "ROOT.ML"; |
|
8 |
|
9 Makefile -- compiles the files under Poly/ML or SML of New Jersey |
|
10 |
|
11 ex.ML -- files containing examples. To execute them, enter an ML image |
|
12 containing LCF and type: use "ex.ML"; |
|
13 |
|
14 Useful references on LCF: |
|
15 |
|
16 Lawrence C. Paulson, |
|
17 Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987) |
|
18 |