# HG changeset patch
# User lcp
# Date 796640294 -7200
# Node ID deb999e33c62aa653e9274539805380fac0d6880
# Parent  8317adb1c44449d62ef0ee12021431353b1bfa8f
Tried the new addss in a proof.

diff -r 8317adb1c444 -r deb999e33c62 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Fri Mar 31 02:00:29 1995 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Mar 31 10:58:14 1995 +0200
@@ -412,10 +412,8 @@
 goalw CardinalArith.thy [inj_def]
  "!!K. Ord(K) ==>	\
 \ (lam z:K*K. split(%x y. <x Un y, <x, y>>, z)) : inj(K*K, K*K*K)";
-by (safe_tac ZF_cs);
-by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI]
-                    addSEs [split_type]) 1);
-by (asm_full_simp_tac ZF_ss 1);
+by (fast_tac (ZF_cs addss ZF_ss
+		    addIs [lam_type, Un_least_lt RS ltD, ltI]) 1);
 qed "csquare_lam_inj";
 
 goalw CardinalArith.thy [csquare_rel_def]