src/HOL/Set.thy
changeset 17715 68583762ebdb
parent 17702 ea88ddeafabe
child 17784 5cbb52f2c478
     1.1 --- a/src/HOL/Set.thy	Thu Sep 29 12:33:26 2005 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Sep 29 12:43:40 2005 +0200
     1.3 @@ -1175,7 +1175,8 @@
     1.4  lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
     1.5    by blast
     1.6  
     1.7 -lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]
     1.8 +lemmas empty_not_insert = insert_not_empty [symmetric, standard]
     1.9 +declare empty_not_insert [simp]
    1.10  
    1.11  lemma insert_absorb: "a \<in> A ==> insert a A = A"
    1.12    -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}