changeset 17441 | 5b5feca0344a |
parent 10466 | 78168ca70469 |
child 19761 | 5cd82054c2c6 |
--- a/src/CTT/ROOT.ML Fri Sep 16 21:02:15 2005 +0200 +++ b/src/CTT/ROOT.ML Fri Sep 16 23:01:29 2005 +0200 @@ -10,13 +10,6 @@ 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*)