# HG changeset patch
# User wenzelm
# Date 1152035387 -7200
# Node ID fe69952f09f6f1ba2d0d84e4f3bdec69f668240b
# Parent  a4332e71c1deb5abb675364a9c872ec6c87d3780
added ex/Guess.thy;

diff -r a4332e71c1de -r fe69952f09f6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 04 18:39:59 2006 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 04 19:49:47 2006 +0200
@@ -633,7 +633,7 @@
 $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Abstract_NAT.thy ex/Antiquote.thy	\
   ex/BT.thy ex/BinEx.thy ex/Classical.thy ex/Chinese.thy 		\
   Library/Commutative_Ring.thy ex/Commutative_RingEx.thy		\
-  ex/Commutative_Ring_Complete.thy ex/Hebrew.thy			\
+  ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy		\
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy	\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
   ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/MT.ML		\
diff -r a4332e71c1de -r fe69952f09f6 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue Jul 04 18:39:59 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jul 04 19:49:47 2006 +0200
@@ -9,6 +9,7 @@
 
 time_use_thy "Higher_Order_Logic";
 time_use_thy "Abstract_NAT";
+time_use_thy "Guess";
 
 time_use_thy "Recdefs";
 time_use_thy "InductiveInvariant_examples";