author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
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"; |