# HG changeset patch
# User paulson
# Date 843747145 -7200
# Node ID e329b36d9136399294458a17b96eeba3acd79afe
# Parent  5079fdf938ddddb23662463e3ffa420441f50f53
Ran expandshort; used stac instead of ssubst

diff -r 5079fdf938dd -r e329b36d9136 src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Fix.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -51,7 +51,7 @@
 by (etac contrapos 1);
 by (rtac po_trans 1);
 by (assume_tac 2);
-by (rtac (napplyBzero RS ssubst) 1);
+by (stac napplyBzero 1);
 by (rtac po_cong 1 THEN rtac po_bot 1);
 qed "npo_INCL";
 
@@ -117,8 +117,8 @@
 
 val [p1,p2,p3] = goal CCL.thy
     "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
-by (rtac (p2 RS cond_eta RS ssubst) 1);
-by (rtac (p3 RS cond_eta RS ssubst) 1);
+by (stac (p2 RS cond_eta) 1);
+by (stac (p3 RS cond_eta) 1);
 by (rtac (p1 RS (po_lam RS iffD2)) 1);
 qed "po_eta";
 
@@ -184,7 +184,7 @@
 by (rtac fix_ind 1);
 by (rewtac idgen_def);
 by (REPEAT_SOME (ares_tac [allI]));
-by (rtac (applyBbot RS ssubst) 1);
+by (stac applyBbot 1);
 by (resolve_tac prems 1);
 br (applyB RS ssubst )1;
 by (res_inst_tac [("t","xa")] term_case 1);
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/Gfp.ML
--- a/src/CCL/Gfp.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Gfp.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -85,7 +85,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 5079fdf938dd -r e329b36d9136 src/CCL/Term.ML
--- a/src/CCL/Term.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Term.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -56,13 +56,13 @@
 val rawBs = caseBs @ [applyB,applyBbot];
 
 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
-           (fn _ => [rtac (letrecB RS ssubst) 1,
+           (fn _ => [stac letrecB 1,
                      simp_tac (CCL_ss addsimps rawBs) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
            (fn _ => [simp_tac (CCL_ss addsimps rawBs 
-                               setloop (rtac (letrecB RS ssubst))) 1]);
+                               setloop (stac letrecB)) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
 val ifBtrue    = mk_beta_rl "if true then t else u = t";
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/Trancl.ML
--- a/src/CCL/Trancl.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Trancl.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -86,14 +86,14 @@
 
 (*Reflexivity of rtrancl*)
 goal Trancl.thy "<a,a> : r^*";
-by (rtac (rtrancl_unfold RS ssubst) 1);
+by (stac rtrancl_unfold 1);
 by (fast_tac comp_cs 1);
 qed "rtrancl_refl";
 
 (*Closure under composition with r*)
 val prems = goal Trancl.thy
     "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
-by (rtac (rtrancl_unfold RS ssubst) 1);
+by (stac rtrancl_unfold 1);
 by (fast_tac (comp_cs addIs prems) 1);
 qed "rtrancl_into_rtrancl";
 
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/Type.ML
--- a/src/CCL/Type.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/Type.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -302,7 +302,7 @@
 val prems = goal Type.thy 
     "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
 by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
-by (rtac (letrecB RS ssubst) 1);
+by (stac letrecB 1);
 by (rewtac cons_def);
 by (fast_tac type_cs 1);
 result();
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/coinduction.ML
--- a/src/CCL/coinduction.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/coinduction.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -7,7 +7,7 @@
 *)
 
 val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
-by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
+by (stac (mono RS lfp_Tarski) 1);
 by (rtac prem 1);
 qed "lfpI";
 
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/ex/Stream.ML
--- a/src/CCL/ex/Stream.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/ex/Stream.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -108,7 +108,7 @@
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
                               napplyBzero RS sym RS arg_cong]) 1);
 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
-by (rtac (napply_f RS ssubst) 1 THEN atac 1);
+by (stac napply_f 1 THEN atac 1);
 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
 by (fast_tac type_cs 1);
 qed "iter1_iter2_eq";
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/genrec.ML
--- a/src/CCL/genrec.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/genrec.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -14,7 +14,7 @@
 \    letrec g x be h(x,g) in g(a) : D(a)";
 by (rtac (major RS rev_mp) 1);
 by (rtac (wf_wf RS wfd_induct) 1);
-by (rtac (letrecB RS ssubst) 1);
+by (stac letrecB 1);
 by (rtac impI 1);
 by (eresolve_tac prems 1);
 by (rtac ballI 1);
@@ -35,7 +35,7 @@
 \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
 by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
-by (rtac (SPLITB RS ssubst) 1);
+by (stac SPLITB 1);
 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
 by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
diff -r 5079fdf938dd -r e329b36d9136 src/CCL/subset.ML
--- a/src/CCL/subset.ML	Thu Sep 26 15:49:54 1996 +0200
+++ b/src/CCL/subset.ML	Thu Sep 26 16:12:25 1996 +0200
@@ -121,4 +121,4 @@
 
 val set_ss = FOL_ss addcongs set_congs
                     delsimps (ex_simps @ all_simps)  (*NO miniscoping*)
-		    addsimps mem_rews;
+                    addsimps mem_rews;