added ex/Guess.thy;
authorwenzelm
Tue Jul 04 19:49:47 2006 +0200 (2006-07-04)
changeset 19997fe69952f09f6
parent 19996 a4332e71c1de
child 19998 c8018518e112
added ex/Guess.thy;
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 04 18:39:59 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 04 19:49:47 2006 +0200
     1.3 @@ -633,7 +633,7 @@
     1.4  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Abstract_NAT.thy ex/Antiquote.thy	\
     1.5    ex/BT.thy ex/BinEx.thy ex/Classical.thy ex/Chinese.thy 		\
     1.6    Library/Commutative_Ring.thy ex/Commutative_RingEx.thy		\
     1.7 -  ex/Commutative_Ring_Complete.thy ex/Hebrew.thy			\
     1.8 +  ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy		\
     1.9    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy	\
    1.10    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
    1.11    ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/MT.ML		\
     2.1 --- a/src/HOL/ex/ROOT.ML	Tue Jul 04 18:39:59 2006 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jul 04 19:49:47 2006 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  
     2.5  time_use_thy "Higher_Order_Logic";
     2.6  time_use_thy "Abstract_NAT";
     2.7 +time_use_thy "Guess";
     2.8  
     2.9  time_use_thy "Recdefs";
    2.10  time_use_thy "InductiveInvariant_examples";