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.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.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.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);
```