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