# 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