--- a/src/HOL/IsaMakefile Fri Oct 07 22:59:19 2005 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 07 22:59:21 2005 +0200
@@ -611,7 +611,7 @@
ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML \
ex/Recdefs.thy ex/Records.thy ex/Reflected_Presburger.thy \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
- ex/StringEx.thy ex/Tarski.thy ex/Tuple.thy ex/document/root.bib \
+ ex/StringEx.thy ex/Tarski.thy ex/document/root.bib \
ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/set.thy \
ex/svc_funcs.ML ex/svc_test.ML ex/svc_test.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/ex/ROOT.ML Fri Oct 07 22:59:19 2005 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Oct 07 22:59:21 2005 +0200
@@ -17,7 +17,6 @@
setmp proofs 2 time_use_thy "Hilbert_Classical";
time_use_thy "Antiquote";
time_use_thy "Multiquote";
-time_use_thy "Tuple";
time_use_thy "NatSum";
time_use_thy "Intuitionistic";