--- 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 \
--- 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";