author | clasohm |
Thu, 16 Sep 1993 12:20:38 +0200 | |
changeset 0 | a5a9c433f639 |
child 72 | 099d949fe467 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: LCF/ROOT |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
Adds LCF to a database containing First-Order Logic. |
|
7 |
||
8 |
This theory is based on Lawrence Paulson's book Logic and Computation. |
|
9 |
*) |
|
10 |
||
11 |
val banner = "Logic for Computable Functions (in FOL)"; |
|
12 |
writeln banner; |
|
13 |
||
14 |
print_depth 1; |
|
15 |
use_thy "lcf"; |
|
16 |
use"simpdata.ML"; |
|
17 |
use"pair.ML"; |
|
18 |
use"fix.ML"; |
|
19 |
||
20 |
val LCF_build_completed = (); (*indicate successful build*) |