| changeset 50705 | 0e943b33d907 |
| parent 46075 | 0054a9513b37 |
| child 53015 | a1119cf551e8 |
--- a/src/HOL/Metis_Examples/Message.thy Thu Jan 03 17:10:12 2013 +0100 +++ b/src/HOL/Metis_Examples/Message.thy Thu Jan 03 17:28:55 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A" by (metis Un_commute Un_left_absorb)