--- a/src/HOL/IsaMakefile Fri Mar 11 15:21:13 2011 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 11 15:21:13 2011 +0100
@@ -469,8 +469,9 @@
Library/While_Combinator.thy Library/Zorn.thy \
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
Library/reflection.ML Library/reify_data.ML \
- Library/LSC.thy $(SRC)/HOL/Tools/LSC/lazysmallcheck.ML \
- $(SRC)/HOL/Tools/LSC/LazySmallCheck.hs \
+ Library/Quickcheck_Narrowing.thy \
+ Tools/Quickcheck/narrowing_generators.ML \
+ Tools/Quickcheck/Narrowing_Engine.hs \
Library/document/root.bib Library/document/root.tex
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
@@ -617,7 +618,7 @@
Number_Theory/UniqueFactorization.thy \
Number_Theory/ROOT.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
-
+
## HOL-Old_Number_Theory
@@ -1039,11 +1040,11 @@
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/LSC_Examples.thy \
ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
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/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \