--- 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 *}
--- 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 *}