src/HOL/ex/MT.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4353 d565d2197a5f
     1.1 --- a/src/HOL/ex/MT.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4  by (rtac eval_fun_mono 1);
     1.5  by (rewtac eval_fun_def);
     1.6  by (dtac CollectD 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (ALLGOALS (resolve_tac prems));
    1.10  by (ALLGOALS (Blast_tac));
    1.11  qed "eval_ind0";
    1.12 @@ -336,7 +336,7 @@
    1.13  by (rtac elab_fun_mono 1);
    1.14  by (rewtac elab_fun_def);
    1.15  by (dtac CollectD 1);
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (ALLGOALS (resolve_tac prems));
    1.19  by (ALLGOALS (Blast_tac));
    1.20  qed "elab_ind0";
    1.21 @@ -387,7 +387,7 @@
    1.22  by (rtac elab_fun_mono 1);
    1.23  by (rewtac elab_fun_def);
    1.24  by (dtac CollectD 1);
    1.25 -by (safe_tac (claset()));
    1.26 +by Safe_tac;
    1.27  by (ALLGOALS (resolve_tac prems));
    1.28  by (ALLGOALS (Blast_tac));
    1.29  qed "elab_elim0";
    1.30 @@ -552,7 +552,7 @@
    1.31  by (rewtac hasty_fun_def);
    1.32  by (dtac CollectD 1);
    1.33  by (fold_goals_tac [hasty_fun_def]);
    1.34 -by (safe_tac (claset()));
    1.35 +by Safe_tac;
    1.36  by (REPEAT (ares_tac prems 1));
    1.37  qed "hasty_rel_elim0";
    1.38  
    1.39 @@ -690,7 +690,7 @@
    1.40  \   |] ==> \
    1.41  \   v_const(c_app c1 c2) hasty t";
    1.42  by (dtac elab_app_elim 1);
    1.43 -by (safe_tac (claset()));
    1.44 +by Safe_tac;
    1.45  by (rtac hasty_const 1);
    1.46  by (rtac isof_app 1);
    1.47  by (rtac hasty_elim_const 1);
    1.48 @@ -711,7 +711,7 @@
    1.49  \   |] ==> \
    1.50  \   v hasty t";
    1.51  by (dtac elab_app_elim 1);
    1.52 -by (safe_tac (claset()));
    1.53 +by Safe_tac;
    1.54  by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
    1.55  by (assume_tac 1);
    1.56  by (etac impE 1);
    1.57 @@ -721,7 +721,7 @@
    1.58  by (etac impE 1);
    1.59  by (assume_tac 1);
    1.60  by (dtac hasty_elim_clos 1);
    1.61 -by (safe_tac (claset()));
    1.62 +by Safe_tac;
    1.63  by (dtac elab_fn_elim 1);
    1.64  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
    1.65  qed "consistency_app2";
    1.66 @@ -733,7 +733,7 @@
    1.67  (* Proof by induction on the structure of evaluations *)
    1.68  
    1.69  by (rtac (major RS eval_ind) 1);
    1.70 -by (safe_tac (claset()));
    1.71 +by Safe_tac;
    1.72  by (DEPTH_SOLVE 
    1.73      (ares_tac [consistency_const, consistency_var, consistency_fn,
    1.74                 consistency_fix, consistency_app1, consistency_app2] 1));
    1.75 @@ -746,7 +746,7 @@
    1.76  val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
    1.77    "ve isofenv te ==> ve hastyenv te";
    1.78  by (cut_facts_tac prems 1);
    1.79 -by (safe_tac (claset()));
    1.80 +by Safe_tac;
    1.81  by (etac allE 1);
    1.82  by (etac impE 1);
    1.83  by (assume_tac 1);