Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added ex/Guess.thy;
authorwenzelm
Tue, 04 Jul 2006 19:49:47 +0200
changeset 19997 fe69952f09f6
parent 19996 a4332e71c1de
child 19998 c8018518e112
added ex/Guess.thy;
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions 
--- 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		\
--- 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";
isabelle