changeset 2033 | 639de962ded4 |
parent 1461 | 6bcb44e4d6e5 |
child 2469 | b50b8c0eec01 |
--- a/src/ZF/OrderType.ML Thu Sep 26 12:50:48 1996 +0200 +++ b/src/ZF/OrderType.ML Thu Sep 26 15:14:23 1996 +0200 @@ -116,7 +116,7 @@ goalw OrderType.thy [ordertype_def] "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; -by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); +by (stac ([ordermap_type, subset_refl] MRS image_fun) 1); by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); by (rewrite_goals_tac [Transset_def,well_ord_def]);