Ran expandshort; used stac instead of ssubst
authorpaulson
Thu Sep 26 16:38:02 1996 +0200 (1996-09-26)
changeset 203662ff902eeffc
parent 2035 e329b36d9136
child 2037 2c2a95cbb5c9
Ran expandshort; used stac instead of ssubst
src/HOL/Gfp.ML
src/HOL/IMP/Denotation.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Gfp.ML	Thu Sep 26 16:12:25 1996 +0200
     1.2 +++ b/src/HOL/Gfp.ML	Thu Sep 26 16:38:02 1996 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  by (rtac prem 1);
     1.5  by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
     1.6  by (rtac (mono RS monoD) 1);
     1.7 -by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
     1.8 +by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
     1.9  by (rtac Un_upper2 1);
    1.10  qed "coinduct3_lemma";
    1.11  
     2.1 --- a/src/HOL/IMP/Denotation.ML	Thu Sep 26 16:12:25 1996 +0200
     2.2 +++ b/src/HOL/IMP/Denotation.ML	Thu Sep 26 16:38:02 1996 +0200
     2.3 @@ -32,9 +32,9 @@
     2.4  auto();
     2.5  (* while *)
     2.6  by (rewtac Gamma_def);
     2.7 -by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
     2.8 +by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
     2.9  by (Fast_tac 1);
    2.10 -by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
    2.11 +by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
    2.12  by (Fast_tac 1);
    2.13  
    2.14  qed "com1";
     3.1 --- a/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:12:25 1996 +0200
     3.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:38:02 1996 +0200
     3.3 @@ -182,7 +182,7 @@
     3.4  \    ==> (UN x:X. b(x)) : B";
     3.5  by (cut_facts_tac prems 1);
     3.6  by (safe_tac (!claset));
     3.7 -by (rtac (localize UN_equiv_class RS ssubst) 1);
     3.8 +by (stac (localize UN_equiv_class) 1);
     3.9  by (REPEAT (ares_tac prems 1));
    3.10  qed "UN_equiv_class_type";
    3.11  
     4.1 --- a/src/HOL/Integ/Integ.ML	Thu Sep 26 16:12:25 1996 +0200
     4.2 +++ b/src/HOL/Integ/Integ.ML	Thu Sep 26 16:38:02 1996 +0200
     4.3 @@ -26,9 +26,9 @@
     4.4  \       x1 + y3 = x3 + y1";
     4.5  by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1);
     4.6  by (rtac (add_left_commute RS trans) 1);
     4.7 -by (rtac (eqb RS ssubst) 1);
     4.8 +by (stac eqb 1);
     4.9  by (rtac (add_left_commute RS trans) 1);
    4.10 -by (rtac (eqa RS ssubst) 1);
    4.11 +by (stac eqa 1);
    4.12  by (rtac (add_left_commute) 1);
    4.13  qed "integ_trans_lemma";
    4.14  
    4.15 @@ -63,7 +63,7 @@
    4.16  qed "intrel_iff";
    4.17  
    4.18  goal Integ.thy "(x,x): intrel";
    4.19 -by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
    4.20 +by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
    4.21  qed "intrel_refl";
    4.22  
    4.23  goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
    4.24 @@ -400,7 +400,7 @@
    4.25  by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
    4.26  by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
    4.27  by (asm_simp_tac (!simpset addsimps ([add_mult_distrib2,zmult] @ 
    4.28 -				     add_ac @ mult_ac)) 1);
    4.29 +                                     add_ac @ mult_ac)) 1);
    4.30  qed "zmult_assoc";
    4.31  
    4.32  (*For AC rewriting*)
    4.33 @@ -418,7 +418,7 @@
    4.34  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
    4.35  by (asm_simp_tac 
    4.36      (!simpset addsimps ([add_mult_distrib2, zadd, zmult] @ 
    4.37 -			add_ac @ mult_ac)) 1);
    4.38 +                        add_ac @ mult_ac)) 1);
    4.39  qed "zadd_zmult_distrib";
    4.40  
    4.41  val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
    4.42 @@ -625,7 +625,7 @@
    4.43  bind_thm ("zless_irrefl", (zless_not_refl RS notE));
    4.44  
    4.45  goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
    4.46 -by(fast_tac (!claset addEs [zless_irrefl]) 1);
    4.47 +by (fast_tac (!claset addEs [zless_irrefl]) 1);
    4.48  qed "zless_not_refl2";
    4.49  
    4.50  
     5.1 --- a/src/HOL/simpdata.ML	Thu Sep 26 16:12:25 1996 +0200
     5.2 +++ b/src/HOL/simpdata.ML	Thu Sep 26 16:38:02 1996 +0200
     5.3 @@ -23,7 +23,8 @@
     5.4  fun auto_tac (cs,ss) = 
     5.5      ALLGOALS (asm_full_simp_tac ss) THEN
     5.6      REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
     5.7 -    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
     5.8 +    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
     5.9 +    prune_params_tac;
    5.10  
    5.11  fun Auto_tac() = auto_tac (!claset, !simpset);
    5.12