# HG changeset patch
# User lcp
# Date 786893938 -3600
# Node ID 66cdfde4ec5db0065cfe1d645bcd222a67ed7225
# Parent  59c0a821e4688d9ba6c7855a36220d4afc11b986
not_well_ord_iso_pred: removed needless quantifier

diff -r 59c0a821e468 -r 66cdfde4ec5d src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Dec 08 14:18:31 1994 +0100
+++ b/src/ZF/Order.ML	Thu Dec 08 14:38:58 1994 +0100
@@ -73,6 +73,18 @@
 by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1);
 qed "ord_iso_converse";
 
+(*Rewriting with bijections and converse (function inverse)*)
+val bij_ss = ZF_ss setsolver (type_auto_tac [bij_is_fun RS apply_type, 
+					     bij_converse_bij])
+		   addsimps [right_inverse_bij, left_inverse_bij];
+
+(*Symmetry of the order-isomorphism relation*)
+goalw Order.thy [ord_iso_def] 
+    "!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
+by (safe_tac ZF_cs);
+by (ALLGOALS (asm_full_simp_tac bij_ss));
+val ord_iso_sym = result();
+
 val major::premx::premy::prems = goalw Order.thy [linear_def]
     "[| linear(A,r);  x:A;  y:A;  \
 \       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
@@ -119,8 +131,7 @@
 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
                      of a well-ordering*)
 goal Order.thy
-    "!!r. [| well_ord(A,r);  x:A |] ==> \
-\         ALL f. f ~: ord_iso(A, r, pred(A,x,r), r)";
+    "!!r. [| well_ord(A,r);  x:A |] ==> f ~: ord_iso(A, r, pred(A,x,r), r)";
 by (safe_tac ZF_cs);
 by (metacut_tac not_well_ord_iso_pred_lemma 1);
 by (REPEAT_SOME assume_tac);