changeset 46635 | cde737f9c911 |
parent 45450 | dc2236b19a3d |
child 46638 | fc315796794e |
--- a/src/HOL/Predicate_Compile.thy Thu Feb 23 21:16:54 2012 +0100 +++ b/src/HOL/Predicate_Compile.thy Thu Feb 23 21:25:59 2012 +0100 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports New_Random_Sequence Quickcheck_Exhaustive +imports Predicate New_Random_Sequence Quickcheck_Exhaustive uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_compilations.ML"