Modified proofs for new claset primitives. The problem is that they enforce
authorlcp
Fri Apr 28 11:31:33 1995 +0200 (1995-04-28)
changeset 1075848bf2e18dff
parent 1074 d60f203eeddf
child 1076 68f088887f48
Modified proofs for new claset primitives. The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.
src/ZF/CardinalArith.ML
src/ZF/Coind/Map.ML
     1.1 --- a/src/ZF/CardinalArith.ML	Fri Apr 28 11:24:32 1995 +0200
     1.2 +++ b/src/ZF/CardinalArith.ML	Fri Apr 28 11:31:33 1995 +0200
     1.3 @@ -633,9 +633,9 @@
     1.4  
     1.5  goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))";
     1.6  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
     1.7 -by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
     1.8 +by (fast_tac (ZF_cs addSIs [Ord_ordertype]) 2);
     1.9  by (rewtac Transset_def);
    1.10 -by (safe_tac ZF_cs);
    1.11 +by (safe_tac subset_cs);
    1.12  by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1);
    1.13  by (safe_tac ZF_cs);
    1.14  by (rtac UN_I 1);
     2.1 --- a/src/ZF/Coind/Map.ML	Fri Apr 28 11:24:32 1995 +0200
     2.2 +++ b/src/ZF/Coind/Map.ML	Fri Apr 28 11:31:33 1995 +0200
     2.3 @@ -79,19 +79,19 @@
     2.4  goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
     2.5    "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
     2.6  by (safe_tac ZF_cs);
     2.7 -by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
     2.8 +by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
     2.9 +by (fast_tac ZF_cs 1);
    2.10  by (fast_tac ZF_cs 1);
    2.11 -by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
    2.12  by (fast_tac ZF_cs 1);
    2.13 +
    2.14  by (rtac (excluded_middle RS disjE) 1);
    2.15  by (etac image_Sigma1 1);
    2.16 -by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
    2.17 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    2.18 -by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    2.19 +by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    2.20 +by (asm_full_simp_tac
    2.21 + (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    2.22  by (safe_tac FOL_cs);
    2.23 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    2.24 -by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    2.25 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    2.26 +by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
    2.27 +by (ALLGOALS (asm_full_simp_tac ZF_ss));
    2.28  by (fast_tac ZF_cs 1);
    2.29  qed "pmap_owrI";
    2.30