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 New_Random_Sequence |
8 imports New_Random_Sequence Quickcheck_Exhaustive |
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_compilations.ML" |
11 "Tools/Predicate_Compile/predicate_compile_compilations.ML" |
12 "Tools/Predicate_Compile/core_data.ML" |
12 "Tools/Predicate_Compile/core_data.ML" |
13 "Tools/Predicate_Compile/mode_inference.ML" |
13 "Tools/Predicate_Compile/mode_inference.ML" |