src/ZF/OrderType.ML
changeset 2033 639de962ded4
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
equal deleted inserted replaced
2032:1bbf1bdcaf56 2033:639de962ded4
   114 by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
   114 by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
   115 qed "Ord_ordermap";
   115 qed "Ord_ordermap";
   116 
   116 
   117 goalw OrderType.thy [ordertype_def]
   117 goalw OrderType.thy [ordertype_def]
   118     "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
   118     "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
   119 by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
   119 by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
   120 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   120 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   121 by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
   121 by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
   122 by (rewrite_goals_tac [Transset_def,well_ord_def]);
   122 by (rewrite_goals_tac [Transset_def,well_ord_def]);
   123 by (safe_tac ZF_cs);
   123 by (safe_tac ZF_cs);
   124 by (ordermap_elim_tac 1);
   124 by (ordermap_elim_tac 1);