# HG changeset patch # User paulson # Date 1127990620 -7200 # Node ID 68583762ebdb507fd5a4daa0e115c7aece861ca9 # Parent 1bdef3df973563abc74382507455f799996676db a name for empty_not_insert diff -r 1bdef3df9735 -r 68583762ebdb src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Sep 29 12:33:26 2005 +0200 +++ b/src/HOL/Set.thy Thu Sep 29 12:43:40 2005 +0200 @@ -1175,7 +1175,8 @@ lemma insert_not_empty [simp]: "insert a A \ {}" by blast -lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard] +lemmas empty_not_insert = insert_not_empty [symmetric, standard] +declare empty_not_insert [simp] lemma insert_absorb: "a \ A ==> insert a A = A" -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}