author | wenzelm |
Thu, 19 Oct 2000 21:22:05 +0200 | |
changeset 10276 | 75e2c6cb4153 |
parent 6349 | f7750d816c21 |
child 10466 | 78168ca70469 |
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 "~~/src/Provers/typedsimp.ML"; use "rew.ML"; use_thy "Arith"; use_thy "Bool"; print_depth 8;