declare defn rules;

--- a/src/FOL/IFOL.thy	Tue Jan 31 00:39:44 2006 +0100
+++ b/src/FOL/IFOL.thy	Tue Jan 31 00:43:14 2006 +0100
@@ -265,6 +265,7 @@
 qed
 
 lemmas [symmetric, rulify] = atomize_all atomize_imp
+  and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
 
 
 subsection {* Calculational rules *}