src/ZF/Coind/Map.ML
changeset 1075 848bf2e18dff
parent 1020 76d72126a9e7
child 1461 6bcb44e4d6e5
     1.1 --- a/src/ZF/Coind/Map.ML	Fri Apr 28 11:24:32 1995 +0200
     1.2 +++ b/src/ZF/Coind/Map.ML	Fri Apr 28 11:31:33 1995 +0200
     1.3 @@ -79,19 +79,19 @@
     1.4  goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
     1.5    "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
     1.6  by (safe_tac ZF_cs);
     1.7 -by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
     1.8 +by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
     1.9 +by (fast_tac ZF_cs 1);
    1.10  by (fast_tac ZF_cs 1);
    1.11 -by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
    1.12  by (fast_tac ZF_cs 1);
    1.13 +
    1.14  by (rtac (excluded_middle RS disjE) 1);
    1.15  by (etac image_Sigma1 1);
    1.16 -by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
    1.17 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.18 -by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    1.19 +by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    1.20 +by (asm_full_simp_tac
    1.21 + (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    1.22  by (safe_tac FOL_cs);
    1.23 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.24 -by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    1.25 -by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.26 +by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
    1.27 +by (ALLGOALS (asm_full_simp_tac ZF_ss));
    1.28  by (fast_tac ZF_cs 1);
    1.29  qed "pmap_owrI";
    1.30