equal
deleted
inserted
replaced
19 ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML" |
19 ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML" |
20 ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML" |
20 ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML" |
21 ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML" |
21 ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML" |
22 ML_file "Tools/Predicate_Compile/predicate_compile.ML" |
22 ML_file "Tools/Predicate_Compile/predicate_compile.ML" |
23 |
23 |
24 setup Predicate_Compile.setup |
|
25 |
24 |
26 subsection {* Set membership as a generator predicate *} |
25 subsection {* Set membership as a generator predicate *} |
27 |
26 |
28 text {* |
27 text {* |
29 Introduce a new constant for membership to allow |
28 Introduce a new constant for membership to allow |