src/FOL/IFOL.thy

--- a/src/FOL/IFOL.thy	Sun Oct 14 22:08:29 2001 +0200
+++ b/src/FOL/IFOL.thy	Sun Oct 14 22:15:07 2001 +0200
@@ -158,4 +158,6 @@
   thus "x == y" by (rule eq_reflection)
 qed
 
+declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
+
 end