author | wenzelm |
Sat, 05 Feb 2000 16:58:58 +0100 | |
changeset 8197 | baab8e487fad |
parent 6349 | f7750d816c21 |
child 9000 | c20d58286a51 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: LCF/ROOT |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Tobias Nipkow |
0 | 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; |
|
121 | 15 |
use_thy "LCF"; |
0 | 16 |
use"simpdata.ML"; |
4905 | 17 |
use_thy"pair"; |
18 |
use_thy"fix"; |