--- a/src/HOL/IsaMakefile Thu Aug 11 09:15:45 2011 +0200
+++ b/src/HOL/IsaMakefile Thu Aug 11 09:41:21 2011 +0200
@@ -1052,7 +1052,6 @@
ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
- ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
@@ -1060,7 +1059,7 @@
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
ex/Quickcheck_Narrowing_Examples.thy \
- ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
+ ex/Quicksort.thy ex/ROOT.ML ex/Records.thy \
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
ex/sledgehammer_tactics.ML ex/Sqrt.thy \