| author | aspinall | 
| Fri, 03 Sep 2004 00:35:38 +0200 | |
| changeset 15175 | b62f7b493360 | 
| parent 9000 | c20d58286a51 | 
| child 17247 | 6927a62c77dc | 
| permissions | -rw-r--r-- | 
| 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 First-Order 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"; |