changeset 44928 | 7ef6505bde7f |
parent 44890 | 22f665a2e91c |
child 45231 | d85a2fdc586c |
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 14 10:55:07 2011 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 14 10:08:52 2011 -0400 @@ -41,7 +41,7 @@ declare Int_def[code_pred_inline] declare eq_reflection[OF Un_def, code_pred_inline] -declare eq_reflection[OF UNION_def, code_pred_inline] +declare eq_reflection[OF UNION_eq, code_pred_inline] lemma Diff[code_pred_inline]: "(A - B) = (%x. A x \<and> \<not> B x)"