src/ZF/CardinalArith.ML
changeset 1075 848bf2e18dff
parent 989 deb999e33c62
child 1090 8ab69b3e396b
--- a/src/ZF/CardinalArith.ML	Fri Apr 28 11:24:32 1995 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Apr 28 11:31:33 1995 +0200
@@ -633,9 +633,9 @@
 
 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+by (fast_tac (ZF_cs addSIs [Ord_ordertype]) 2);
 by (rewtac Transset_def);
-by (safe_tac ZF_cs);
+by (safe_tac subset_cs);
 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1);
 by (safe_tac ZF_cs);
 by (rtac UN_I 1);