# HG changeset patch
# User wenzelm
# Date 1138664594 -3600
# Node ID 38269ef5175a7284e1657fa5422ecff2e55a75ad
# Parent  9089cdb4c5fdb0ff500c2b1f2961132202e34b7d
declare defn rules;

diff -r 9089cdb4c5fd -r 38269ef5175a src/FOL/IFOL.thy
--- 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 *}