| changeset 58823 | 513268cb2178 |
| parent 55543 | f0ef75c6c0d8 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Predicate_Compile.thy Wed Oct 29 15:07:53 2014 +0100 +++ b/src/HOL/Predicate_Compile.thy Wed Oct 29 15:15:17 2014 +0100 @@ -21,7 +21,6 @@ ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML" ML_file "Tools/Predicate_Compile/predicate_compile.ML" -setup Predicate_Compile.setup subsection {* Set membership as a generator predicate *}