src/HOL/Set.thy
changeset 25287 094dab519ff5
parent 24730 a87d8d31abc0
child 25360 b8251517f508
     1.1 --- a/src/HOL/Set.thy	Mon Nov 05 17:48:51 2007 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Nov 05 18:18:39 2007 +0100
     1.3 @@ -780,6 +780,8 @@
     1.4    show "x \<notin> A - {x}" by blast
     1.5  qed
     1.6  
     1.7 +lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
     1.8 +by auto
     1.9  
    1.10  subsubsection {* Singletons, using insert *}
    1.11