removed obsolete ex/Tuple.thy;
authorwenzelm
Fri, 07 Oct 2005 22:59:21 +0200
changeset 17783 4175daa1286c
parent 17782 b3846df9d643
child 17784 5cbb52f2c478
removed obsolete ex/Tuple.thy;
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
--- 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";