equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>A compiler for predicates defined by introduction rules\<close> |
5 section \<open>A compiler for predicates defined by introduction rules\<close> |
6 |
6 |
7 theory Predicate_Compile |
7 theory Predicate_Compile |
8 imports Random_Sequence Quickcheck_Exhaustive |
8 imports Random_Sequence Quickcheck_Exhaustive |
9 keywords "code_pred" :: thy_goal and "values" :: diag |
9 keywords |
|
10 "code_pred" :: thy_goal and |
|
11 "values" :: diag |
10 begin |
12 begin |
11 |
13 |
12 ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML" |
14 ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML" |
13 ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML" |
15 ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML" |
14 ML_file "Tools/Predicate_Compile/core_data.ML" |
16 ML_file "Tools/Predicate_Compile/core_data.ML" |