author  wenzelm 
Thu, 14 Oct 1999 15:04:36 +0200  
changeset 7866  3ccaa11b6df9 
parent 6349  f7750d816c21 
child 9000  c20d58286a51 
permissions  rwrr 
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 FirstOrder 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"; 