author | wenzelm |
Sun, 29 Nov 1998 13:14:45 +0100 | |
changeset 5986 | 6ebbc9e7cc20 |
parent 4905 | be73ddff6c5a |
child 6349 | f7750d816c21 |
permissions | -rw-r--r-- |
(* Title: LCF/ROOT ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge Adds LCF to a database containing 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"; val LCF_build_completed = (); (*indicate successful build*)