author  clasohm 
Tue, 16 Nov 1993 14:10:19 +0100  
changeset 121  d392174734e9 
parent 72  099d949fe467 
child 1296  ae31bb7774a7 
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; 

121  15 
use_thy "LCF"; 
0  16 
use"simpdata.ML"; 
17 
use"pair.ML"; 

18 
use"fix.ML"; 

19 

20 
val LCF_build_completed = (); (*indicate successful build*) 