# HG changeset patch
# User lcp
# Date 787936850 -3600
# Node ID de2d8a63256dc41619a573346dce555f76f1f463
# Parent  a32b420c33d44aef3c4756caeb4568f8541a5457
ord_iso_rvimage: new

diff -r a32b420c33d4 -r de2d8a63256d src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Tue Dec 20 15:58:52 1994 +0100
+++ b/src/ZF/OrderArith.ML	Tue Dec 20 16:20:50 1994 +0100
@@ -237,3 +237,8 @@
 by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1);
 by (fast_tac (ZF_cs addSIs [linear_rvimage]) 1);
 qed "well_ord_rvimage";
+
+goalw OrderArith.thy [ord_iso_def]
+    "!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
+by (asm_full_simp_tac (ZF_ss addsimps [rvimage_iff]) 1);
+qed "ord_iso_rvimage";