author  clasohm 
Thu, 16 Sep 1993 12:20:38 +0200  
changeset 0  a5a9c433f639 
child 72  099d949fe467 
permissions  rwrr 
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 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; 

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*) 