changeset 34948 | 2d5f2a9f7601 |
parent 33265 | 01c9c6dbd890 |
child 35879 | 99818df5b8f5 |
--- a/src/HOL/Predicate_Compile.thy Sat Jan 16 21:14:15 2010 +0100 +++ b/src/HOL/Predicate_Compile.thy Wed Jan 20 11:56:45 2010 +0100 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports Quickcheck +imports Random_Sequence Quickcheck uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_core.ML" @@ -18,4 +18,4 @@ setup Predicate_Compile.setup -end \ No newline at end of file +end