# HG changeset patch
# User wenzelm
# Date 1128718761 -7200
# Node ID 4175daa1286c9f03066132c96a5a0547f684fd0d
# Parent  b3846df9d643ab06fc7f8701a159c3ad86e38c1a
removed obsolete ex/Tuple.thy;

diff -r b3846df9d643 -r 4175daa1286c src/HOL/IsaMakefile
--- 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
diff -r b3846df9d643 -r 4175daa1286c src/HOL/ex/ROOT.ML
--- 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";