# HG changeset patch
# User haftmann
# Date 1174639247 -3600
# Node ID e2d378a97905d56d2115fe520de7dc5418d378af
# Parent  22b638460a13051dacad2fa5628918e98b0bc279
removed outdated example

diff -r 22b638460a13 -r e2d378a97905 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 23 09:40:45 2007 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 23 09:40:47 2007 +0100
@@ -617,12 +617,12 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
-  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy 	\
+  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
   ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
-  ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
-  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
-  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy	\
-  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy	\
+  ex/Codegenerator.thy ex/Codegenerator_Rat.thy                                 \
+  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy                             \
+  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy                     \
+  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.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 22b638460a13 -r e2d378a97905 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:45 2007 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:47 2007 +0100
@@ -8,7 +8,6 @@
 no_document use_thy "GCD";
 
 no_document time_use_thy "Classpackage";
-no_document time_use_thy "CodeCollections";
 no_document time_use_thy "CodeEval";
 no_document time_use_thy "CodeRandom";
 no_document time_use_thy "Codegenerator_Rat";