author  berghofe 
Fri, 11 Jul 2003 14:55:17 +0200  
changeset 14102  8af7334af4b3 
parent 9000  c20d58286a51 
child 17247  6927a62c77dc 
permissions  rwrr 
9000  1 
(* Title: LCF/ROOT.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Tobias Nipkow 
0  4 
Copyright 1992 University of Cambridge 
5 

9000  6 
LCF on top of FirstOrder Logic. 
0  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"; 