removed outdated example
authorhaftmann
Fri Mar 23 09:40:47 2007 +0100 (2007-03-23)
changeset 22505e2d378a97905
parent 22504 22b638460a13
child 22506 c78f1d924bfe
removed outdated example
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Mar 23 09:40:45 2007 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 23 09:40:47 2007 +0100
     1.3 @@ -617,12 +617,12 @@
     1.4  
     1.5  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
     1.6    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
     1.7 -  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy 	\
     1.8 +  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
     1.9    ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			 	\
    1.10 -  ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
    1.11 -  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy	\
    1.12 -  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy	\
    1.13 -  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy	\
    1.14 +  ex/Codegenerator.thy ex/Codegenerator_Rat.thy                                 \
    1.15 +  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy                             \
    1.16 +  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy                     \
    1.17 +  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy                       \
    1.18    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
    1.19    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
    1.20    ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/MT.ML			\
     2.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:45 2007 +0100
     2.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 23 09:40:47 2007 +0100
     2.3 @@ -8,7 +8,6 @@
     2.4  no_document use_thy "GCD";
     2.5  
     2.6  no_document time_use_thy "Classpackage";
     2.7 -no_document time_use_thy "CodeCollections";
     2.8  no_document time_use_thy "CodeEval";
     2.9  no_document time_use_thy "CodeRandom";
    2.10  no_document time_use_thy "Codegenerator_Rat";