author | clasohm |
Tue, 24 Oct 1995 14:50:24 +0100 | |
changeset 1296 | ae31bb7774a7 |
parent 121 | d392174734e9 |
child 1361 | 90d615b599d9 |
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"pair.ML"; use"fix.ML"; make_chart (); (*make HTML chart*) val LCF_build_completed = (); (*indicate successful build*)