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