author | wenzelm |
Wed, 09 Jul 1997 17:00:34 +0200 | |
changeset 3511 | da4dd8b7ced4 |
parent 2237 | f01ac387e82b |
child 3929 | 3553fcfa2c7e |
permissions | -rw-r--r-- |
(* Title: CTT/ROOT ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Adds Constructive Type Theory to a database containing pure Isabelle. Should be executed in the subdirectory CTT. *) val banner = "Constructive Type Theory"; writeln banner; print_depth 1; use_thy "CTT"; use "../Provers/typedsimp.ML"; use "rew.ML"; use_thy "Arith"; use_thy "Bool"; print_depth 8; val CTT_build_completed = (); (*indicate successful build*)