src/HOL/IOA/Solve.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4477 b3e5857d8d99
     1.1 --- a/src/HOL/IOA/Solve.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/IOA/Solve.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
     1.5  
     1.6    by (simp_tac(simpset() addsimps [has_trace_def])1);
     1.7 -  by (safe_tac (claset()));
     1.8 +  by Safe_tac;
     1.9  
    1.10    (* choose same trace, therefore same NF *)
    1.11    by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
    1.12 @@ -32,7 +32,7 @@
    1.13  
    1.14    (* Now show that it's an execution *)
    1.15    by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
    1.16 -  by (safe_tac (claset()));
    1.17 +  by Safe_tac;
    1.18  
    1.19    (* Start states map to start states *)
    1.20    by (dtac bspec 1);
    1.21 @@ -40,7 +40,7 @@
    1.22  
    1.23    (* Show that it's an execution fragment *)
    1.24    by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
    1.25 -  by (safe_tac (claset()));
    1.26 +  by Safe_tac;
    1.27  
    1.28    by (eres_inst_tac [("x","snd ex n")] allE 1);
    1.29    by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
    1.30 @@ -51,7 +51,7 @@
    1.31  (* Lemmata *)
    1.32  
    1.33  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    1.34 -  by(fast_tac (claset() addDs prems) 1);
    1.35 +  by (fast_tac (claset() addDs prems) 1);
    1.36  val imp_conj_lemma = result();
    1.37  
    1.38  
    1.39 @@ -120,7 +120,7 @@
    1.40  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
    1.41  by (simp_tac (simpset() addsimps [par_def]) 1);
    1.42  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
    1.43 -by (rtac (expand_if RS ssubst) 1);
    1.44 +by (stac expand_if 1);
    1.45  by (rtac conjI 1);
    1.46  by (rtac impI 1); 
    1.47  by (etac disjE 1);
    1.48 @@ -142,7 +142,7 @@
    1.49  by (Fast_tac 2);
    1.50  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
    1.51                   addsplits [expand_if]) 1);
    1.52 -by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    1.53 +by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    1.54          asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.55                                        comp2_reachable])1));
    1.56  qed"fxg_is_weak_pmap_of_product_IOA";
    1.57 @@ -174,8 +174,8 @@
    1.58  by (rtac imp_conj_lemma 1);
    1.59  by (simp_tac (simpset() addsimps [rename_def]) 1);
    1.60  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
    1.61 -by (safe_tac (claset()));
    1.62 -by (rtac (expand_if RS ssubst) 1);
    1.63 +by Safe_tac;
    1.64 +by (stac expand_if 1);
    1.65   by (rtac conjI 1);
    1.66   by (rtac impI 1);
    1.67   by (etac disjE 1);