changeset 45450 | dc2236b19a3d |
parent 40052 | ea46574ca815 |
child 46635 | cde737f9c911 |
--- a/src/HOL/Predicate_Compile.thy Fri Nov 11 08:32:44 2011 +0100 +++ b/src/HOL/Predicate_Compile.thy Fri Nov 11 08:32:45 2011 +0100 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports New_Random_Sequence +imports New_Random_Sequence Quickcheck_Exhaustive uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_compilations.ML"