src/HOLCF/Cfun3.ML

--- a/src/HOLCF/Cfun3.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cfun3.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -17,11 +17,11 @@
         (strip_tac 1),
         (rtac (expand_fun_eq RS iffD2) 1),
         (strip_tac 1),
-        (rtac (thelub_cfun RS ssubst) 1),
+        (stac thelub_cfun 1),
         (atac 1),
-        (rtac (Cfunapp2 RS ssubst) 1),
+        (stac Cfunapp2 1),
         (etac cont_lubcfun 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
         (rtac refl 1)
         ]);
@@ -52,7 +52,7 @@
         (cut_facts_tac prems 1),
         (rtac trans 1),
         (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (etac (monofun_fapp1 RS ch2ch_monofun) 1),
         (rtac refl 1)
         ]);
@@ -137,12 +137,12 @@
         (cut_facts_tac prems 1),
         (rtac monofunI 1),
         (strip_tac 1),
-        (rtac (less_cfun RS ssubst) 1),
-        (rtac (less_fun RS ssubst) 1),
+        (stac less_cfun 1),
+        (stac less_fun 1),
         (rtac allI 1),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (etac spec 1),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (etac spec 1),
         (etac ((hd (tl prems)) RS spec RS monofunE RS spec RS spec RS mp) 1)
         ]);
@@ -162,7 +162,7 @@
         (etac spec 1),
         (rtac contlubI 1),
         (strip_tac 1),
-        (rtac (thelub_cfun RS ssubst) 1),
+        (stac thelub_cfun 1),
         (rtac (cont2mono_LAM RS ch2ch_monofun) 1),
         (atac 1),
         (rtac (cont2mono RS allI) 1),
@@ -170,7 +170,7 @@
         (atac 1),
         (res_inst_tac [("f","fabs")] arg_cong 1),
         (rtac ext 1),
-        (rtac (beta_cfun RS ext RS ssubst) 1),
+        (stac (beta_cfun RS ext) 1),
         (etac spec 1),
         (rtac (cont2contlub RS contlubE 
                 RS spec RS mp ) 1),
@@ -208,9 +208,9 @@
 qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)`x = (UU::'b)"
  (fn prems =>
         [
-        (rtac (inst_cfun_pcpo RS ssubst) 1),
+        (stac inst_cfun_pcpo 1),
         (rewtac UU_cfun_def),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (cont_tac 1),
         (rtac refl 1)
         ]);
@@ -243,15 +243,15 @@
         (rtac (less_fun RS iffD2) 1),
         (strip_tac 1),
         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (atac 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (atac 1),
         (rtac monofun_cfun_fun 1),
         (atac 1),
         (hyp_subst_tac 1),
-        (rtac (Istrictify1 RS ssubst) 1),
-        (rtac (Istrictify1 RS ssubst) 1),
+        (stac Istrictify1 1),
+        (stac Istrictify1 1),
         (rtac refl_less 1)
         ]);
 
@@ -261,15 +261,15 @@
         (rtac monofunI 1),
         (strip_tac 1),
         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (etac notUU_I 1),
         (atac 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (atac 1),
         (rtac monofun_cfun_arg 1),
         (atac 1),
         (hyp_subst_tac 1),
-        (rtac (Istrictify1 RS ssubst) 1),
+        (stac Istrictify1 1),
         (rtac minimal 1)
         ]);
 
@@ -281,22 +281,22 @@
         (strip_tac 1),
         (rtac (expand_fun_eq RS iffD2) 1),
         (strip_tac 1),
-        (rtac (thelub_fun RS ssubst) 1),
+        (stac thelub_fun 1),
         (etac (monofun_Istrictify1 RS ch2ch_monofun) 1),
         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (atac 1),
-        (rtac (Istrictify2 RS ext RS ssubst) 1),
+        (stac (Istrictify2 RS ext) 1),
         (atac 1),
-        (rtac (thelub_cfun RS ssubst) 1),
+        (stac thelub_cfun 1),
         (atac 1),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (rtac cont_lubcfun 1),
         (atac 1),
         (rtac refl 1),
         (hyp_subst_tac 1),
-        (rtac (Istrictify1 RS ssubst) 1),
-        (rtac (Istrictify1 RS ext RS ssubst) 1),
+        (stac Istrictify1 1),
+        (stac (Istrictify1 RS ext) 1),
         (rtac (chain_UU_I_inverse RS sym) 1),
         (rtac (refl RS allI) 1)
         ]);
@@ -310,7 +310,7 @@
         (res_inst_tac [("t","lub(range(Y))")] subst 1),
         (rtac sym 1),
         (atac 1),
-        (rtac (Istrictify1 RS ssubst) 1),
+        (stac Istrictify1 1),
         (rtac sym 1),
         (rtac chain_UU_I_inverse 1),
         (strip_tac 1),
@@ -320,7 +320,7 @@
         (atac 1),
         (atac 1),
         (rtac Istrictify1 1),
-        (rtac (Istrictify2 RS ssubst) 1),
+        (stac Istrictify2 1),
         (atac 1),
         (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1),
         (rtac contlub_cfun_arg 1),
@@ -354,12 +354,12 @@
         "strictify`f`UU=UU"
  (fn prems =>
         [
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (cont_tac 1),
         (rtac cont_Istrictify2 1),
         (rtac cont2cont_CF1L 1),
         (rtac cont_Istrictify1 1),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (rtac cont_Istrictify2 1),
         (rtac Istrictify1 1)
         ]);
@@ -368,12 +368,12 @@
         "~x=UU ==> strictify`f`x=f`x"
  (fn prems =>
         [
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (cont_tac 1),
         (rtac cont_Istrictify2 1),
         (rtac cont2cont_CF1L 1),
         (rtac cont_Istrictify1 1),
-        (rtac (beta_cfun RS ssubst) 1),
+        (stac beta_cfun 1),
         (rtac cont_Istrictify2 1),
         (rtac Istrictify2 1),
         (resolve_tac prems 1)