| changeset 45607 | 16b4f5774621 |
| parent 45152 | e877b76c72bd |
| child 45625 | 750c5a47400b |
--- a/src/HOL/Set.thy Sun Nov 20 21:07:06 2011 +0100 +++ b/src/HOL/Set.thy Sun Nov 20 21:07:10 2011 +0100 @@ -1107,7 +1107,7 @@ lemma insert_not_empty [simp]: "insert a A \<noteq> {}" by blast -lemmas empty_not_insert = insert_not_empty [symmetric, standard] +lemmas empty_not_insert = insert_not_empty [symmetric] declare empty_not_insert [simp] lemma insert_absorb: "a \<in> A ==> insert a A = A"