changeset 36046 | c3946372f556 |
parent 36032 | dfd30b5b4e73 |
child 40052 | ea46574ca815 |
--- a/src/HOL/Predicate_Compile.thy Tue Mar 30 15:46:50 2010 -0700 +++ b/src/HOL/Predicate_Compile.thy Wed Mar 31 16:44:41 2010 +0200 @@ -8,6 +8,7 @@ imports New_Random_Sequence uses "Tools/Predicate_Compile/predicate_compile_aux.ML" + "Tools/Predicate_Compile/predicate_compile_compilations.ML" "Tools/Predicate_Compile/predicate_compile_core.ML" "Tools/Predicate_Compile/predicate_compile_data.ML" "Tools/Predicate_Compile/predicate_compile_fun.ML"