bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
(* 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 "Main";
print_depth 8;
Goal "tt : T"; (*leave subgoal package empty*)