# 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 \<noteq> {}"
   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 \<in> A ==> insert a A = A"
   -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}