src/HOL/IsaMakefile
changeset 33250 5c2af18a3237
parent 33210 94ae82a4452f
child 33256 b350516cb1f9
--- a/src/HOL/IsaMakefile	Mon Oct 26 23:27:24 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Oct 27 09:02:22 2009 +0100
@@ -255,6 +255,7 @@
   Map.thy \
   Nat_Numeral.thy \
   Presburger.thy \
+  Predicate_Compile.thy \
   Quickcheck.thy \
   Random.thy \
   Recdef.thy \
@@ -283,6 +284,13 @@
   Tools/numeral_simprocs.ML \
   Tools/numeral_syntax.ML \
   Tools/polyhash.ML \
+  Tools/Predicate_Compile/predicate_compile_aux.ML \
+  Tools/Predicate_Compile/predicate_compile_core.ML \
+  Tools/Predicate_Compile/predicate_compile_data.ML \
+  Tools/Predicate_Compile/predicate_compile_fun.ML \
+  Tools/Predicate_Compile/predicate_compile.ML \
+  Tools/Predicate_Compile/predicate_compile_pred.ML \
+  Tools/Predicate_Compile/predicate_compile_set.ML \
   Tools/quickcheck_generators.ML \
   Tools/Qelim/cooper_data.ML \
   Tools/Qelim/cooper.ML \
@@ -945,7 +953,7 @@
   ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
-  ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy			\
+  ex/Predicate_Compile_ex.thy			\
   ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.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		\