# HG changeset patch
# User lcp
# Date 787421754 -3600
# Node ID 8acbe6f3de2bf068b189d7d5142d7f0c3f0737b3
# Parent  1affbb1c5f1f60f5cae18408985b49808b742155
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
not_well_ord_iso_pred

diff -r 1affbb1c5f1f -r 8acbe6f3de2b src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Wed Dec 14 16:57:55 1994 +0100
+++ b/src/ZF/OrderType.ML	Wed Dec 14 17:15:54 1994 +0100
@@ -231,8 +231,8 @@
 \         |] ==> R";
 by (forward_tac [lt_eq_pred] 1);
 be ltE 1;
-by (rtac (well_ord_Memrel RS not_well_ord_iso_pred RS notE) 1 THEN
-    assume_tac 1 THEN assume_tac 1);
+by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
+    assume_tac 3 THEN assume_tac 1);
 be subst 1;
 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
 (*Combining the two simplifications causes looping*)