new Main.thy as in HOL, ZF
authorpaulson
Tue Nov 14 13:25:59 2000 +0100 (2000-11-14)
changeset 1046678168ca70469
parent 10465 4aa6f8b5cdc4
child 10467 e6e7205e9e91
new Main.thy as in HOL, ZF
src/CTT/Main.thy
src/CTT/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CTT/Main.thy	Tue Nov 14 13:25:59 2000 +0100
     1.3 @@ -0,0 +1,6 @@
     1.4 +
     1.5 +(*theory Main includes everything*)
     1.6 +
     1.7 +theory Main = CTT + Arith + Bool:
     1.8 +
     1.9 +end
     2.1 --- a/src/CTT/ROOT.ML	Mon Nov 13 22:05:57 2000 +0100
     2.2 +++ b/src/CTT/ROOT.ML	Tue Nov 14 13:25:59 2000 +0100
     2.3 @@ -15,7 +15,8 @@
     2.4  use_thy "CTT";
     2.5  use "~~/src/Provers/typedsimp.ML";
     2.6  use "rew.ML";
     2.7 -use_thy "Arith";
     2.8 -use_thy "Bool";
     2.9 +use_thy "Main";
    2.10  
    2.11  print_depth 8;
    2.12 +
    2.13 +Goal "tt : T";  (*leave subgoal package empty*)