--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Apr 30 10:08:00 2012 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Apr 30 12:14:51 2012 +0200
@@ -29,15 +29,7 @@
declare Ball_def[code_pred_inline]
declare Bex_def[code_pred_inline]
-section {* Set operations *}
-
-declare eq_reflection[OF empty_def, code_pred_inline]
-
-declare subset_iff[code_pred_inline]
-
-declare Int_def[code_pred_inline]
-declare eq_reflection[OF Un_def, code_pred_inline]
-declare eq_reflection[OF UNION_eq, code_pred_inline]
+section {* Operations on Predicates *}
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \<and> \<not> B x)"
@@ -51,7 +43,6 @@
"A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
by (auto simp add: fun_eq_iff)
-
section {* Setup for Numerals *}
setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}