| author | oheimb | 
| Tue, 07 Jan 2003 18:08:17 +0100 | |
| changeset 13774 | 77a1e723151d | 
| parent 9000 | c20d58286a51 | 
| child 17247 | 6927a62c77dc | 
| permissions | -rw-r--r-- | 
(* Title: LCF/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge LCF on top of First-Order Logic. This theory is based on Lawrence Paulson's book Logic and Computation. *) val banner = "Logic for Computable Functions (in FOL)"; writeln banner; print_depth 1; use_thy "LCF"; use"simpdata.ML"; use_thy"pair"; use_thy"fix";