Ran expandshort
authorpaulson
Tue Apr 22 11:45:22 1997 +0200 (1997-04-22)
changeset 30080a887d5b6718
parent 3007 e5efa177ee0c
child 3009 38c0b6dbd24f
Ran expandshort
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/W0/W.ML
     1.1 --- a/src/HOL/MiniML/MiniML.ML	Tue Apr 22 11:37:12 1997 +0200
     1.2 +++ b/src/HOL/MiniML/MiniML.ML	Tue Apr 22 11:45:22 1997 +0200
     1.3 @@ -74,8 +74,8 @@
     1.4  \                       else TVar x) o \
     1.5  \                  (%x. if x : free_tv A \
     1.6  \                       then x else n + x)) A)";
     1.7 -by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1);
     1.8 -by (rtac (alpha_A RS ssubst) 1);
     1.9 +by (stac S_o_alpha_type_scheme_list 1);
    1.10 +by (stac alpha_A 1);
    1.11  by (rtac refl 1);
    1.12  qed "S'_A_eq_S'_alpha_A";
    1.13  
     2.1 --- a/src/HOL/MiniML/Type.ML	Tue Apr 22 11:37:12 1997 +0200
     2.2 +++ b/src/HOL/MiniML/Type.ML	Tue Apr 22 11:45:22 1997 +0200
     2.3 @@ -318,9 +318,9 @@
     2.4       "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
     2.5  \     free_tv s1 Un free_tv s2";
     2.6  by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
     2.7 -			     free_tv_subst_var RS subsetD] 
     2.8 -	             addss (!simpset delsimps bex_simps
     2.9 -				     addsimps [cod_def,dom_def])) 1);
    2.10 +                             free_tv_subst_var RS subsetD] 
    2.11 +                     addss (!simpset delsimps bex_simps
    2.12 +                                     addsimps [cod_def,dom_def])) 1);
    2.13  qed "free_tv_comp_subst";
    2.14  
    2.15  goalw thy [o_def] 
    2.16 @@ -481,7 +481,7 @@
    2.17  goal thy "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
    2.18  by (type_scheme.induct_tac "sch" 1);
    2.19  by (ALLGOALS (Asm_full_simp_tac));
    2.20 -by (rewrite_goals_tac [new_tv_def]);
    2.21 +by (rewtac new_tv_def);
    2.22  by (simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
    2.23  by (strip_tac 1);
    2.24  by (case_tac "S nat = TVar nat" 1);
    2.25 @@ -638,7 +638,7 @@
    2.26  by (REPEAT (etac exE 1));
    2.27  by (rename_tac "n2 n1" 1);
    2.28  by (res_inst_tac [("x","(max n1 n2)")] exI 1);
    2.29 -by (rewrite_goals_tac [new_tv_def]);
    2.30 +by (rewtac new_tv_def);
    2.31  by (fast_tac (!claset addIs [less_maxL,less_maxR]) 1);
    2.32  qed "ex_fresh_variable";
    2.33  
     3.1 --- a/src/HOL/MiniML/W.ML	Tue Apr 22 11:37:12 1997 +0200
     3.2 +++ b/src/HOL/MiniML/W.ML	Tue Apr 22 11:45:22 1997 +0200
     3.3 @@ -206,13 +206,13 @@
     3.4  ba 1;
     3.5  ba 1;
     3.6  ba 1;
     3.7 -by (rewrite_goals_tac [new_tv_def]);
     3.8 +by (rewtac new_tv_def);
     3.9  by (Asm_simp_tac 1);
    3.10  by (dtac W_var_ge 1);
    3.11  by (rtac allI 1);
    3.12  by (rename_tac "p" 1);
    3.13  by (strip_tac 1);
    3.14 -by (rewrite_goals_tac [free_tv_subst]);
    3.15 +by (rewtac free_tv_subst);
    3.16  by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
    3.17  fun restrict_prems is tacf =
    3.18    METAHYPS(fn prems =>
    3.19 @@ -494,7 +494,7 @@
    3.20  by (eres_inst_tac [("x","Suc n")] allE 1);
    3.21  by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
    3.22                    unsafe_addss (!simpset addcongs [conj_cong] 
    3.23 -				setloop (split_tac [expand_option_bind]))) 1);
    3.24 +                                setloop (split_tac [expand_option_bind]))) 1);
    3.25  (** LEVEL 19 **)
    3.26  
    3.27  (* case App e1 e2 *)
     4.1 --- a/src/HOL/W0/W.ML	Tue Apr 22 11:37:12 1997 +0200
     4.2 +++ b/src/HOL/W0/W.ML	Tue Apr 22 11:45:22 1997 +0200
     4.3 @@ -174,7 +174,7 @@
     4.4  by (eres_inst_tac [("x","na")] allE 1);
     4.5  by (eres_inst_tac [("x","v")] allE 1);
     4.6  by (fast_tac (HOL_cs addSEs [allE]
     4.7 -	             addIs [cod_app_subst]
     4.8 +                     addIs [cod_app_subst]
     4.9                       addss (!simpset addsimps [less_Suc_eq])) 1);
    4.10  (** LEVEL 12 **)
    4.11  (* case App e1 e2 *)
    4.12 @@ -211,11 +211,11 @@
    4.13  by (dtac (sym RS W_var_geD) 1);
    4.14  by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
    4.15  by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
    4.16 -			    free_tv_app_subst_te RS subsetD,
    4.17 -			    free_tv_app_subst_tel RS subsetD,
    4.18 -			    less_le_trans,subsetD]
    4.19 -	             addSEs [UnE]
    4.20 -		     addss !simpset) 1); 
    4.21 +                            free_tv_app_subst_te RS subsetD,
    4.22 +                            free_tv_app_subst_tel RS subsetD,
    4.23 +                            less_le_trans,subsetD]
    4.24 +                     addSEs [UnE]
    4.25 +                     addss !simpset) 1); 
    4.26  qed_spec_mp "free_tv_W"; 
    4.27  
    4.28  (* Completeness of W w.r.t. has_type *)
    4.29 @@ -370,7 +370,7 @@
    4.30  by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.31  by (dtac (free_tv_app_subst_tel RS subsetD) 1);
    4.32  by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
    4.33 -			    eq_subst_tel_eq_free] 
    4.34 +                            eq_subst_tel_eq_free] 
    4.35         addss ((!simpset addsimps [free_tv_subst,dom_def]))) 1);
    4.36  (** LEVEL 106 **)
    4.37  by (Fast_tac 1);