equal
deleted
inserted
replaced
502 by (REPEAT |
502 by (REPEAT |
503 (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); |
503 (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); |
504 by (asm_simp_tac |
504 by (asm_simp_tac |
505 (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); |
505 (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); |
506 by (rewtac ord_iso_map_def); |
506 by (rewtac ord_iso_map_def); |
507 by (safe_tac (claset() addSEs [UN_E])); |
507 by Safe_tac; |
508 by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac); |
508 by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac); |
509 qed "ord_iso_map_mono_map"; |
509 qed "ord_iso_map_mono_map"; |
510 |
510 |
511 Goalw [mono_map_def] |
511 Goalw [mono_map_def] |
512 "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |
512 "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ |