src/FOL/IFOL.thy
changeset 11771 b7b100a2de1d
parent 11747 17a6dcd6f3cf
child 11848 6e3017adb8c0
     1.1 --- a/src/FOL/IFOL.thy	Sun Oct 14 22:08:29 2001 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sun Oct 14 22:15:07 2001 +0200
     1.3 @@ -158,4 +158,6 @@
     1.4    thus "x == y" by (rule eq_reflection)
     1.5  qed
     1.6  
     1.7 +declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
     1.8 +
     1.9  end