src/HOL/IsaMakefile
changeset 33250 5c2af18a3237
parent 33210 94ae82a4452f
child 33256 b350516cb1f9
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 26 23:27:24 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 09:02:22 2009 +0100
     1.3 @@ -255,6 +255,7 @@
     1.4    Map.thy \
     1.5    Nat_Numeral.thy \
     1.6    Presburger.thy \
     1.7 +  Predicate_Compile.thy \
     1.8    Quickcheck.thy \
     1.9    Random.thy \
    1.10    Recdef.thy \
    1.11 @@ -283,6 +284,13 @@
    1.12    Tools/numeral_simprocs.ML \
    1.13    Tools/numeral_syntax.ML \
    1.14    Tools/polyhash.ML \
    1.15 +  Tools/Predicate_Compile/predicate_compile_aux.ML \
    1.16 +  Tools/Predicate_Compile/predicate_compile_core.ML \
    1.17 +  Tools/Predicate_Compile/predicate_compile_data.ML \
    1.18 +  Tools/Predicate_Compile/predicate_compile_fun.ML \
    1.19 +  Tools/Predicate_Compile/predicate_compile.ML \
    1.20 +  Tools/Predicate_Compile/predicate_compile_pred.ML \
    1.21 +  Tools/Predicate_Compile/predicate_compile_set.ML \
    1.22    Tools/quickcheck_generators.ML \
    1.23    Tools/Qelim/cooper_data.ML \
    1.24    Tools/Qelim/cooper.ML \
    1.25 @@ -945,7 +953,7 @@
    1.26    ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
    1.27    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
    1.28    ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
    1.29 -  ex/Predicate_Compile.thy ex/Predicate_Compile_ex.thy			\
    1.30 +  ex/Predicate_Compile_ex.thy			\
    1.31    ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    1.32    ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
    1.33    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\