# HG changeset patch
# User lcp
# Date 797163065 -7200
# Node ID 75110179587d3d8e2a1db4cfb813298279a5a6f7
# Parent  8bec0698d58c7edcf4d45e9f35d38cb9b14b86d8
Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac

diff -r 8bec0698d58c -r 75110179587d src/ZF/Order.ML
--- a/src/ZF/Order.ML	Thu Apr 06 12:08:43 1995 +0200
+++ b/src/ZF/Order.ML	Thu Apr 06 12:11:05 1995 +0200
@@ -525,15 +525,15 @@
 (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
 goalw Order.thy [ord_iso_map_def]
   "!!B. [| well_ord(A,r);  well_ord(B,s);    		\
-\          x: A;  x ~: domain(ord_iso_map(A,r,B,s)) 	\
-\       |] ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, x, r)";
-by (step_tac (ZF_cs addSIs [predI]) 1);
-(*Case analysis on  xaa vs x in r *)
+\          a: A;  a ~: domain(ord_iso_map(A,r,B,s)) 	\
+\       |] ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)";
+by (safe_tac (ZF_cs addSIs [predI]));
+(*Case analysis on  xaa vs a in r *)
 by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
 by (linear_case_tac 1);
-(*Trivial case: xaa=x*)
-by (fast_tac ZF_cs 1);
-(*Harder case: <x, xaa>: r*)
+(*Trivial case: a=xa*)
+by (fast_tac ZF_cs 2);
+(*Harder case: <a, xa>: r*)
 by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
     REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
 by (forward_tac [ord_iso_restrict_pred] 1  THEN