equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* A compiler for predicates defined by introduction rules *} |
5 header {* A compiler for predicates defined by introduction rules *} |
6 |
6 |
7 theory Predicate_Compile |
7 theory Predicate_Compile |
8 imports Random_Sequence Quickcheck |
8 imports New_Random_Sequence |
9 uses |
9 uses |
10 "Tools/Predicate_Compile/predicate_compile_aux.ML" |
10 "Tools/Predicate_Compile/predicate_compile_aux.ML" |
11 "Tools/Predicate_Compile/predicate_compile_core.ML" |
11 "Tools/Predicate_Compile/predicate_compile_core.ML" |
12 "Tools/Predicate_Compile/predicate_compile_data.ML" |
12 "Tools/Predicate_Compile/predicate_compile_data.ML" |
13 "Tools/Predicate_Compile/predicate_compile_fun.ML" |
13 "Tools/Predicate_Compile/predicate_compile_fun.ML" |