src/ZF/OrderType.ML
changeset 788 8acbe6f3de2b
parent 782 200a16083201
child 803 4c8333ab3eae
equal deleted inserted replaced
787:1affbb1c5f1f 788:8acbe6f3de2b
   229 goal OrderType.thy
   229 goal OrderType.thy
   230     "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j))	\
   230     "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j))	\
   231 \         |] ==> R";
   231 \         |] ==> R";
   232 by (forward_tac [lt_eq_pred] 1);
   232 by (forward_tac [lt_eq_pred] 1);
   233 be ltE 1;
   233 be ltE 1;
   234 by (rtac (well_ord_Memrel RS not_well_ord_iso_pred RS notE) 1 THEN
   234 by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
   235     assume_tac 1 THEN assume_tac 1);
   235     assume_tac 3 THEN assume_tac 1);
   236 be subst 1;
   236 be subst 1;
   237 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
   237 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
   238 (*Combining the two simplifications causes looping*)
   238 (*Combining the two simplifications causes looping*)
   239 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
   239 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
   240 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]  
   240 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]