# HG changeset patch
# User paulson
# Date 843748682 -7200
# Node ID 62ff902eeffc7a2d79176f7808459c1badd8fd4d
# Parent  e329b36d9136399294458a17b96eeba3acd79afe
Ran expandshort; used stac instead of ssubst

diff -r e329b36d9136 -r 62ff902eeffc src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Thu Sep 26 16:12:25 1996 +0200
+++ b/src/HOL/Gfp.ML	Thu Sep 26 16:38:02 1996 +0200
@@ -87,7 +87,7 @@
 by (rtac prem 1);
 by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
 by (rtac (mono RS monoD) 1);
-by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
+by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
 by (rtac Un_upper2 1);
 qed "coinduct3_lemma";
 
diff -r e329b36d9136 -r 62ff902eeffc src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Thu Sep 26 16:12:25 1996 +0200
+++ b/src/HOL/IMP/Denotation.ML	Thu Sep 26 16:38:02 1996 +0200
@@ -32,9 +32,9 @@
 auto();
 (* while *)
 by (rewtac Gamma_def);
-by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
 by (Fast_tac 1);
-by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
 by (Fast_tac 1);
 
 qed "com1";
diff -r e329b36d9136 -r 62ff902eeffc src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:12:25 1996 +0200
+++ b/src/HOL/Integ/Equiv.ML	Thu Sep 26 16:38:02 1996 +0200
@@ -182,7 +182,7 @@
 \    ==> (UN x:X. b(x)) : B";
 by (cut_facts_tac prems 1);
 by (safe_tac (!claset));
-by (rtac (localize UN_equiv_class RS ssubst) 1);
+by (stac (localize UN_equiv_class) 1);
 by (REPEAT (ares_tac prems 1));
 qed "UN_equiv_class_type";
 
diff -r e329b36d9136 -r 62ff902eeffc src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Thu Sep 26 16:12:25 1996 +0200
+++ b/src/HOL/Integ/Integ.ML	Thu Sep 26 16:38:02 1996 +0200
@@ -26,9 +26,9 @@
 \       x1 + y3 = x3 + y1";
 by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1);
 by (rtac (add_left_commute RS trans) 1);
-by (rtac (eqb RS ssubst) 1);
+by (stac eqb 1);
 by (rtac (add_left_commute RS trans) 1);
-by (rtac (eqa RS ssubst) 1);
+by (stac eqa 1);
 by (rtac (add_left_commute) 1);
 qed "integ_trans_lemma";
 
@@ -63,7 +63,7 @@
 qed "intrel_iff";
 
 goal Integ.thy "(x,x): intrel";
-by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
+by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
 qed "intrel_refl";
 
 goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
@@ -400,7 +400,7 @@
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
 by (asm_simp_tac (!simpset addsimps ([add_mult_distrib2,zmult] @ 
-				     add_ac @ mult_ac)) 1);
+                                     add_ac @ mult_ac)) 1);
 qed "zmult_assoc";
 
 (*For AC rewriting*)
@@ -418,7 +418,7 @@
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac 
     (!simpset addsimps ([add_mult_distrib2, zadd, zmult] @ 
-			add_ac @ mult_ac)) 1);
+                        add_ac @ mult_ac)) 1);
 qed "zadd_zmult_distrib";
 
 val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
@@ -625,7 +625,7 @@
 bind_thm ("zless_irrefl", (zless_not_refl RS notE));
 
 goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
-by(fast_tac (!claset addEs [zless_irrefl]) 1);
+by (fast_tac (!claset addEs [zless_irrefl]) 1);
 qed "zless_not_refl2";
 
 
diff -r e329b36d9136 -r 62ff902eeffc src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Sep 26 16:12:25 1996 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 26 16:38:02 1996 +0200
@@ -23,7 +23,8 @@
 fun auto_tac (cs,ss) = 
     ALLGOALS (asm_full_simp_tac ss) THEN
     REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN
-    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
+    REPEAT (FIRSTGOAL (best_tac (cs addss ss))) THEN
+    prune_params_tac;
 
 fun Auto_tac() = auto_tac (!claset, !simpset);