proper theory context for mesontest2;
authorwenzelm
Fri Nov 10 19:08:30 2000 +0100 (2000-11-10)
changeset 104402074e62da354
parent 10439 be2dc95dfe98
child 10441 d727c39c4a4b
proper theory context for mesontest2;
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
src/HOL/ex/mesontest2.ML
src/HOL/ex/mesontest2.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Nov 10 19:07:17 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 10 19:08:30 2000 +0100
     1.3 @@ -462,8 +462,8 @@
     1.4    ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
     1.5    ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \
     1.6    ex/Ring.thy ex/StringEx.ML ex/StringEx.thy ex/Tarski.ML \
     1.7 -  ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
     1.8 -  ex/mesontest2.ML ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy
     1.9 +  ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
    1.10 +  ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.12  
    1.13  
     2.1 --- a/src/HOL/ex/ROOT.ML	Fri Nov 10 19:07:17 2000 +0100
     2.2 +++ b/src/HOL/ex/ROOT.ML	Fri Nov 10 19:08:30 2000 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  time_use_thy "NatSum";
     2.5  time_use     "cla.ML";
     2.6  time_use     "mesontest.ML";
     2.7 -time_use     "mesontest2.ML";
     2.8 +time_use_thy "mesontest2";
     2.9  time_use_thy "BT";
    2.10  time_use_thy "AVL";
    2.11  time_use_thy "InSort";
     3.1 --- a/src/HOL/ex/mesontest2.ML	Fri Nov 10 19:07:17 2000 +0100
     3.2 +++ b/src/HOL/ex/mesontest2.ML	Fri Nov 10 19:08:30 2000 +0100
     3.3 @@ -11,9 +11,7 @@
     3.4  (*All but the fastest are ignored to reduce build time*)
     3.5  val even_hard_ones = false;
     3.6  
     3.7 -(*Product_Type.thy instead of HOL.thy regards arguments as tuples.
     3.8 -  But Main.thy would allow clashes with many other constants*)
     3.9 -fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
    3.10 +fun prove (s,tac) = prove_goal (the_context ()) s (fn [] => [tac]);
    3.11  
    3.12  fun prove_hard arg = if even_hard_ones then prove arg else TrueI;
    3.13  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/mesontest2.thy	Fri Nov 10 19:08:30 2000 +0100
     4.3 @@ -0,0 +1,9 @@
     4.4 +
     4.5 +(*Theory Product_Type instead of HOL regards arguments as tuples.
     4.6 +  But theory Main would allow clashes with many other constants.*)
     4.7 +
     4.8 +theory mesontest2 = Product_Type:
     4.9 +
    4.10 +hide const inverse divide
    4.11 +
    4.12 +end