diff -r 0b5c5f568d74 -r 349d41ffa378 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Fri Dec 16 13:30:34 1994 +0100
+++ b/src/ZF/Order.ML	Fri Dec 16 13:43:01 1994 +0100
@@ -245,20 +245,6 @@
 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1);
 qed "linear_ord_iso";
 
-(*FOR FOL/IFOL.ML*)
-fun iff_tac prems i =
-    resolve_tac (prems RL [iffE]) i THEN
-    REPEAT1 (eresolve_tac [asm_rl,mp] i);
-
-(*Reversed congruence rule!*)
-val conj_cong2 = prove_goal 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)) ]);
-
 goalw Order.thy [wf_on_def, wf_def, ord_iso_def]
     "!!A B r. [| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
 (*reversed &-congruence rule handles context of membership in A*)