# HG changeset patch
# User wenzelm
# Date 1138559018 -3600
# Node ID 6ab4de872a7028fa9b94ff110014096cd29049f1
# Parent  f1315d11805933618b764b61005c621b6b6a1c41
declare 'defn' rules;

diff -r f1315d118059 -r 6ab4de872a70 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jan 28 17:29:49 2006 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 29 19:23:38 2006 +0100
@@ -904,6 +904,7 @@
 qed
 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
+  and [symmetric, defn] = atomize_all atomize_imp atomize_eq
 
 
 subsubsection {* Classical Reasoner setup *}
diff -r f1315d118059 -r 6ab4de872a70 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jan 28 17:29:49 2006 +0100
+++ b/src/HOL/Set.thy	Sun Jan 29 19:23:38 2006 +0100
@@ -1011,7 +1011,8 @@
     "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
   by (simp only: Ball_def atomize_all atomize_imp)
 
-declare atomize_ball [symmetric, rulify]
+lemmas [symmetric, rulify] = atomize_ball
+  and [symmetric, defn] = atomize_ball
 
 
 subsection {* Further set-theory lemmas *}