# HG changeset patch # User bulwahn # Date 1307601135 -7200 # Node ID d1265a4d8ae1f74be9f23923e9a696c3aa5a9b42 # Parent 3bc28ce6986c5d4d46d4bc28903a233f0357921d adapting IsaMakefile diff -r 3bc28ce6986c -r d1265a4d8ae1 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jun 09 08:32:14 2011 +0200 +++ b/src/HOL/IsaMakefile Thu Jun 09 08:32:15 2011 +0200 @@ -281,6 +281,7 @@ Predicate_Compile.thy \ Quickcheck.thy \ Quickcheck_Exhaustive.thy \ + Quickcheck_Narrowing.thy \ Quotient.thy \ Random.thy \ Random_Sequence.thy \ @@ -348,6 +349,9 @@ Tools/Quickcheck/exhaustive_generators.ML \ Tools/Quickcheck/random_generators.ML \ Tools/Quickcheck/quickcheck_common.ML \ + Tools/Quickcheck/narrowing_generators.ML \ + Tools/Quickcheck/Narrowing_Engine.hs \ + Tools/Quickcheck/PNF_Narrowing_Engine.hs \ Tools/Quotient/quotient_def.ML \ Tools/Quotient/quotient_info.ML \ Tools/Quotient/quotient_tacs.ML \ @@ -479,9 +483,6 @@ Library/While_Combinator.thy Library/Zorn.thy \ $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ Library/reflection.ML Library/reify_data.ML \ - 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