renamed addss to addSss, unsafe_addss to addss, extended auto_tac
authoroheimb
Thu May 15 15:51:09 1997 +0200 (1997-05-15 ago)
changeset 3206a3de7f32728c
parent 3205 816a1f9fd620
child 3207 fe79ad367d77
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu May 15 15:47:19 1997 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu May 15 15:51:09 1997 +0200
     1.3 @@ -279,23 +279,14 @@
     1.4  			premises to all the premises *)
     1.5  
     1.6  (*Add a simpset to a classical set!*)
     1.7 -infix 4 addss;
     1.8 -fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     1.9 -
    1.10 -(*old version, for compatibility with unstable old proofs*)
    1.11 -infix 4 unsafe_addss;
    1.12 -fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
    1.13 +infix 4 addSss addss;
    1.14 +fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
    1.15 +fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
    1.16  
    1.17  fun Addss ss = (claset := !claset addss ss);
    1.18  
    1.19  (*Designed to be idempotent, except if best_tac instantiates variables
    1.20    in some of the subgoals*)
    1.21 -(*old version, for compatibility with unstable old proofs*)
    1.22 -fun unsafe_auto_tac (cs,ss) = 
    1.23 -    ALLGOALS (asm_full_simp_tac ss) THEN
    1.24 -    REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
    1.25 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
    1.26 -    prune_params_tac;
    1.27  
    1.28  type clasimpset = (claset * simpset);
    1.29  
    1.30 @@ -317,10 +308,13 @@
    1.31  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    1.32  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    1.33  
    1.34 -fun auto_tac (cs,ss) = let val cs' = cs addss ss in
    1.35 -EVERY [	TRY (safe_tac cs'),
    1.36 -	REPEAT (FIRSTGOAL (fast_tac cs')),
    1.37 -	prune_params_tac] end;
    1.38 +fun auto_tac (cs,ss) = 
    1.39 +    let val cs' = cs addss ss 
    1.40 +    in  EVERY [TRY (safe_tac cs'),
    1.41 +	       REPEAT (FIRSTGOAL (fast_tac cs')),
    1.42 +               TRY (safe_tac (cs addSss ss)),
    1.43 +	       prune_params_tac] 
    1.44 +    end;
    1.45  
    1.46  fun Auto_tac () = auto_tac (!claset, !simpset);
    1.47  
     2.1 --- a/src/HOL/simpdata.ML	Thu May 15 15:47:19 1997 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Thu May 15 15:51:09 1997 +0200
     2.3 @@ -402,24 +402,14 @@
     2.4  				     safe_asm_full_simp_tac ss;
     2.5  
     2.6  (*Add a simpset to a classical set!*)
     2.7 -infix 4 addss;
     2.8 -fun cs addss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     2.9 -(*old version, for compatibility with unstable old proofs*)
    2.10 -infix 4 unsafe_addss;
    2.11 -fun cs unsafe_addss ss = cs addbefore asm_full_simp_tac ss;
    2.12 +infix 4 addSss addss;
    2.13 +fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
    2.14 +fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
    2.15  
    2.16  fun Addss ss = (claset := !claset addss ss);
    2.17 -(*old version, for compatibility with unstable old proofs*)
    2.18 -fun Unsafe_Addss ss = (claset := !claset unsafe_addss ss);
    2.19  
    2.20  (*Designed to be idempotent, except if best_tac instantiates variables
    2.21    in some of the subgoals*)
    2.22 -(*old version, for compatibility with unstable old proofs*)
    2.23 -fun unsafe_auto_tac (cs,ss) = 
    2.24 -    ALLGOALS (asm_full_simp_tac ss) THEN
    2.25 -    REPEAT   (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
    2.26 -    REPEAT   (FIRSTGOAL (best_tac (cs addss ss))) THEN
    2.27 -    prune_params_tac;
    2.28  
    2.29  type clasimpset = (claset * simpset);
    2.30  
    2.31 @@ -445,6 +435,7 @@
    2.32      let val cs' = cs addss ss 
    2.33      in  EVERY [TRY (safe_tac cs'),
    2.34  	       REPEAT (FIRSTGOAL (fast_tac cs')),
    2.35 +               TRY (safe_tac (cs addSss ss)),
    2.36  	       prune_params_tac] 
    2.37      end;
    2.38