diff -r 5d2a7634da46 -r 0b5c5f568d74 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Thu Dec 15 11:50:53 1994 +0100
+++ b/src/FOL/IFOL.ML	Fri Dec 16 13:30:34 1994 +0100
@@ -150,6 +150,15 @@
       ORELSE  eresolve_tac [iffE,conjE,mp] 1
       ORELSE  iff_tac prems 1)) ]);
 
+(*Reversed congruence rule!   Used in ZF/Order*)
+qed_goal "conj_cong2" IFOL.thy 
+    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"
+ (fn prems =>
+  [ (cut_facts_tac prems 1),
+    (REPEAT  (ares_tac [iffI,conjI] 1
+      ORELSE  eresolve_tac [iffE,conjE,mp] 1
+      ORELSE  iff_tac prems 1)) ]);
+
 qed_goal "disj_cong" IFOL.thy 
     "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
  (fn prems =>