removing obsolete setup for sets now that sets are executable
authorbulwahn
Mon Apr 30 12:14:51 2012 +0200 (2012-04-30)
changeset 47840732ea1f08e3f
parent 47839 3c54878ed67b
child 47841 179b5e7c9803
removing obsolete setup for sets now that sets are executable
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 30 10:08:00 2012 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 30 12:14:51 2012 +0200
     1.3 @@ -29,15 +29,7 @@
     1.4  declare Ball_def[code_pred_inline]
     1.5  declare Bex_def[code_pred_inline]
     1.6  
     1.7 -section {* Set operations *}
     1.8 -
     1.9 -declare eq_reflection[OF empty_def, code_pred_inline]
    1.10 -
    1.11 -declare subset_iff[code_pred_inline]
    1.12 -
    1.13 -declare Int_def[code_pred_inline]
    1.14 -declare eq_reflection[OF Un_def, code_pred_inline]
    1.15 -declare eq_reflection[OF UNION_eq, code_pred_inline]
    1.16 +section {* Operations on Predicates *}
    1.17  
    1.18  lemma Diff[code_pred_inline]:
    1.19    "(A - B) = (%x. A x \<and> \<not> B x)"
    1.20 @@ -51,7 +43,6 @@
    1.21    "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
    1.22    by (auto simp add: fun_eq_iff)
    1.23  
    1.24 -
    1.25  section {* Setup for Numerals *}
    1.26  
    1.27  setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}