# HG changeset patch
# User lcp
# Date 799061493 -7200
# Node ID 848bf2e18dff499557757bba9acf8d887b433e94
# Parent  d60f203eeddf712cf1b92595b6c4e3a21cff69a7
Modified proofs for new claset primitives.  The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

diff -r d60f203eeddf -r 848bf2e18dff src/ZF/CardinalArith.ML
--- 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);
diff -r d60f203eeddf -r 848bf2e18dff src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Fri Apr 28 11:24:32 1995 +0200
+++ b/src/ZF/Coind/Map.ML	Fri Apr 28 11:31:33 1995 +0200
@@ -79,19 +79,19 @@
 goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
   "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
 by (safe_tac ZF_cs);
-by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
+by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
+by (fast_tac ZF_cs 1);
 by (fast_tac ZF_cs 1);
-by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
 by (fast_tac ZF_cs 1);
+
 by (rtac (excluded_middle RS disjE) 1);
 by (etac image_Sigma1 1);
-by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
-by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
+by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
+by (asm_full_simp_tac
+ (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
 by (safe_tac FOL_cs);
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
-by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
-by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
+by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
+by (ALLGOALS (asm_full_simp_tac ZF_ss));
 by (fast_tac ZF_cs 1);
 qed "pmap_owrI";