| changeset 46664 | 1f6c140f9c72 |
| parent 46638 | fc315796794e |
| child 46950 | d0181abdbdac |
--- a/src/HOL/Predicate_Compile.thy Fri Feb 24 22:46:16 2012 +0100 +++ b/src/HOL/Predicate_Compile.thy Fri Feb 24 22:46:44 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"