author | bulwahn |
Mon, 29 Mar 2010 17:30:39 +0200 | |
changeset 36021 | c86fcf44b4c9 |
parent 36020 | 3ee4c29ead7f |
child 36022 | c0fa8499e366 |
--- a/src/HOL/Predicate_Compile.thy Mon Mar 29 17:30:38 2010 +0200 +++ b/src/HOL/Predicate_Compile.thy Mon Mar 29 17:30:39 2010 +0200 @@ -5,7 +5,7 @@ header {* A compiler for predicates defined by introduction rules *} theory Predicate_Compile -imports Random_Sequence Quickcheck +imports New_Random_Sequence uses "Tools/Predicate_Compile/predicate_compile_aux.ML" "Tools/Predicate_Compile/predicate_compile_core.ML"