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