--- a/src/CTT/ROOT.ML Fri Jun 02 16:06:19 2006 +0200
+++ b/src/CTT/ROOT.ML Fri Jun 02 18:15:38 2006 +0200
@@ -1,15 +1,10 @@
-(* Title: CTT/ROOT
+(* Title: CTT/ROOT.ML
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;
use_thy "Main";
-
-Goal "tt : T"; (*leave subgoal package empty*)