changeset 36021 | c86fcf44b4c9 |
parent 35898 | c890a3835d15 |
child 36032 | dfd30b5b4e73 |
--- 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"