# HG changeset patch
# User haftmann
# Date 1206011360 -3600
# Node ID 6d437bde2f1d32cfe9e38ec83c7a452ce0550302
# Parent  d6a508c1690874f3a82bda1f84a4cf684c1c05bf
more antiquotations

diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -110,7 +110,7 @@
 fun inst_conj_all_tac k = EVERY
   [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    REPEAT_DETERM_N k (etac allE 1),
-   simp_tac (HOL_basic_ss addsimps [id_apply]) 1];
+   simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
 
 fun map_term f t u = (case f t u of
       NONE => map_term' f t u | x => x)
@@ -305,7 +305,7 @@
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
-             full_simp_tac (HOL_basic_ss addsimps [id_apply]) 1,
+             full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
              REPEAT (etac conjE 1)])
           [ex] ctxt
       in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
@@ -347,7 +347,7 @@
                     map (fold_rev (NominalPackage.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
-                   Simplifier.simplify (HOL_basic_ss addsimps [id_apply]
+                   Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
                        addsimprocs [NominalPackage.perm_simproc])
                      (Simplifier.simplify eqvt_ss
                        (fold_rev (mk_perm_bool o cterm_of thy)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -959,7 +959,7 @@
                   alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
                   perm_rep_perm_thms)) 1),
                 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
-                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
+                  @{thm expand_fun_eq} :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
         end) (constrs ~~ constr_rep_thms)
       end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -84,6 +84,9 @@
 lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
       |- Calling send p & ~Calling rcv p & cst!p = #clkA   
          --> Enabled (MClkFwd send rcv cst p)"
+  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
+    @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
     thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
     [thm "base_enabled", Pair_inject] 1 *})
@@ -100,10 +103,10 @@
       |- Calling send p & ~Calling rcv p & cst!p = #clkB   
          --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
   apply (tactic {* action_simp_tac @{simpset}
-    [thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
+    [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
   apply (tactic {* action_simp_tac (@{simpset} addsimps
-    [thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
-    [exI] [thm "base_enabled", Pair_inject] 1 *})
+    [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+    [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   done
 
 lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -123,7 +123,7 @@
          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
           rtac (cterm_instantiate inst induction) 1,
           ALLGOALS ObjectLogic.atomize_prems_tac,
-          rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
+          rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -401,7 +401,7 @@
 
         val rewrites = map mk_meta_eq iso_char_thms;
         val inj_thms' = map snd newT_iso_inj_thms @
-          map (fn r => r RS injD) inj_thms;
+          map (fn r => r RS @{thm injD}) inj_thms;
 
         val inj_thm = Goal.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
@@ -425,7 +425,7 @@
                              Lim_inject :: fun_cong :: inj_thms')) 1),
                          atac 1]))])])])]);
 
-        val inj_thms'' = map (fn r => r RS datatype_injI)
+        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
                              (split_conj_thm inj_thm);
 
         val elem_thm = 
@@ -442,7 +442,7 @@
     val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
       ([], map #3 newT_iso_axms) (tl descr);
     val iso_inj_thms = map snd newT_iso_inj_thms @
-      map (fn r => r RS injD) iso_inj_thms_unfolded;
+      map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
 
     (* prove  dt_rep_set_i x --> x : range dt_Rep_i *)
 
@@ -461,7 +461,7 @@
 
     (* all the theorems are proved by one single simultaneous induction *)
 
-    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
+    val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
       iso_inj_thms_unfolded;
 
     val iso_thms = if length descr = 1 then [] else
@@ -470,7 +470,7 @@
            [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq choice_eq ::
-              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
+              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
             rewrite_goals_tac (map symmetric range_eqs),
             REPEAT (EVERY
               [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
@@ -495,7 +495,7 @@
     fun prove_constr_rep_thm eqn =
       let
         val inj_thms = map fst newT_iso_inj_thms;
-        val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
+        val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
       in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
         [resolve_tac inj_thms 1,
          rewrite_goals_tac rewrites,
diff -r d6a508c16908 -r 6d437bde2f1d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Mar 20 12:09:20 2008 +0100
@@ -64,8 +64,8 @@
 val meta_allE = thm "Pure.meta_allE";
 val prop_subst = thm "prop_subst";
 val Pair_sel_convs = [fst_conv,snd_conv];
-val K_record_comp = thm "K_record_comp";
-val K_comp_convs = [o_apply, K_record_comp]
+val K_record_comp = @{thm "K_record_comp"};
+val K_comp_convs = [@{thm o_apply}, K_record_comp]
 
 (** name components **)
 
@@ -2063,7 +2063,7 @@
       in
         prove_standard [assm] concl (fn {prems, ...} =>
           try_param_tac rN induct_scheme 1
-          THEN try_param_tac "more" unit_induct 1
+          THEN try_param_tac "more" @{thm unit_induct} 1
           THEN resolve_tac prems 1)
       end;
     val induct = timeit_msg "record induct proof:" induct_prf;
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -33,7 +33,7 @@
 apply (simp (no_asm) add: is_simulation_def)
 apply (rule conjI)
 txt {* start states *}
-apply (tactic "SELECT_GOAL (safe_tac set_cs) 1")
+apply (auto)[1]
 apply (rule_tac x = " ({},False) " in exI)
 apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def)
 txt {* main-part *}
@@ -42,7 +42,7 @@
 apply (rename_tac k b used c k' b' a)
 apply (induct_tac "a")
 apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 txt {* NEW *}
 apply (rule_tac x = "(used,True)" in exI)
 apply simp
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -106,11 +106,7 @@
 apply simp
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
 txt {* main case *}
-apply (tactic "safe_tac set_cs")
-apply (simp add: is_abstraction_def)
-apply (frule reachable.reachable_n)
-apply assumption
-apply simp
+apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
 done
 
 
@@ -131,8 +127,7 @@
           ==> validIOA C P"
 apply (drule abs_is_weakening)
 apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
 done
 
 
@@ -161,8 +156,7 @@
 apply auto
 apply (drule abs_is_weakening)
 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
 done
 
 
@@ -175,8 +169,7 @@
 apply auto
 apply (drule abs_is_weakening)
 apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "ex" 1 *})
+apply (auto simp add: split_paired_all)
 done
 
 
@@ -185,7 +178,7 @@
 lemma abstraction_is_ref_map:
 "is_abstraction h C A ==> is_ref_map h C A"
 apply (unfold is_abstraction_def is_ref_map_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "(a,h t) >>nil" in exI)
 apply (simp add: move_def)
 done
@@ -223,9 +216,9 @@
                    is_live_abstraction h (C,M) (A,L) |]
                 ==> live_implements (C,M) (A,L)"
 apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "cex_abs h ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
   (* Traces coincide *)
   apply (tactic {* pair_tac "ex" 1 *})
   apply (rule traces_coincide_abs)
@@ -251,9 +244,7 @@
 
 lemma implements_trans:
 "[| A =<| B; B =<| C|] ==> A =<| C"
-apply (unfold ioa_implements_def)
-apply auto
-done
+by (auto simp add: ioa_implements_def)
 
 
 subsection "Abstraction Rules for Automata"
@@ -373,7 +364,7 @@
 apply (tactic {* Seq_Finite_induct_tac 1 *})
 apply blast
 (* main case *)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
 apply (tactic {* pair_tac "ex" 1 *})
 apply (tactic {* Seq_case_simp_tac "y" 1 *})
 (* UU case *)
@@ -425,9 +416,9 @@
 "[| temp_strengthening P Q h |]
        ==> temp_strengthening ([] P) ([] Q) h"
 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
 apply (frule ex2seq_tsuffix)
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
 apply (drule_tac h = "h" in cex_absSeq_tsuffix)
 apply (simp add: ex2seq_abs_cex)
 done
@@ -440,7 +431,7 @@
        ==> temp_strengthening (Init P) (Init Q) h"
 apply (unfold temp_strengthening_def state_strengthening_def
   temp_sat_def satisfies_def Init_def unlift_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (tactic {* pair_tac "ex" 1 *})
 apply (tactic {* Seq_case_simp_tac "y" 1 *})
 apply (tactic {* pair_tac "a" 1 *})
@@ -505,7 +496,7 @@
        ==> temp_strengthening (Next P) (Next Q) h"
 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
 apply simp
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
 apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
@@ -526,7 +517,7 @@
        ==> temp_weakening (Init P) (Init Q) h"
 apply (simp add: temp_weakening_def2 state_weakening_def2
   temp_sat_def satisfies_def Init_def unlift_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (tactic {* pair_tac "ex" 1 *})
 apply (tactic {* Seq_case_simp_tac "y" 1 *})
 apply (tactic {* pair_tac "a" 1 *})
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -399,7 +399,7 @@
       ==> input_enabled (A||B)"
 apply (unfold input_enabled_def)
 apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac set_cs")
+apply (tactic "safe_tac (claset_of @{theory Fun})")
 apply (simp add: inp_is_act)
 prefer 2
 apply (simp add: inp_is_act)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -218,9 +218,7 @@
 
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
 (* main case *)
-apply (rename_tac ss a t)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2)
+apply (auto simp add: trans_of_defs2)
 done
 
 
@@ -234,8 +232,7 @@
 
 apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2)
+apply (auto simp add: trans_of_defs2)
 done
 
 
@@ -249,8 +246,8 @@
 apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   thm "is_exec_frag_def"] 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: trans_of_defs2 actions_asig_comp asig_of_par)
+apply auto
+apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
 done
 
 
@@ -268,10 +265,7 @@
 
 apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   thm "is_exec_frag_def", thm "stutter_def"] 1 *})
-apply (simp add: trans_of_defs1 actions_asig_comp asig_of_par)
-apply (tactic "safe_tac set_cs")
-apply simp
-apply simp
+apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
 done
 
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -237,8 +237,8 @@
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
   thm "sforall_def"] 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
-apply (auto simp add: trans_of_defs2 actions_asig_comp asig_of_par)
+apply auto
+apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
 done
 
 
@@ -260,7 +260,7 @@
 
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
-apply (tactic "safe_tac set_cs")
+apply auto
 
 (* Case y:A, y:B *)
 apply (tactic {* Seq_case_simp_tac "exA" 1 *})
@@ -301,7 +301,7 @@
 fun mkex_induct_tac sch exA exB =
     EVERY1[Seq_induct_tac sch defs,
            SIMPSET' asm_full_simp_tac,
-           SELECT_GOAL (safe_tac set_cs),
+           SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
            Seq_case_simp_tac exA,
            Seq_case_simp_tac exB,
            SIMPSET' asm_full_simp_tac,
@@ -502,7 +502,7 @@
    Filter (%a. a:act B)$sch : schedules B &
    Forall (%x. x:act (A||B)) sch)"
 apply (simp (no_asm) add: schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 (* ==> *)
 apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
 prefer 2
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -200,7 +200,7 @@
     ! schA schB. Forall (%x. x:act (A||B)) tr  
     --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
 apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (simp add: actions_of_par)
 apply (case_tac "a:act A")
 apply (case_tac "a:act B")
@@ -227,7 +227,7 @@
     ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
     --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
 apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
 done
@@ -236,8 +236,7 @@
     ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
     --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
 apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
-apply (tactic "safe_tac set_cs")
-apply simp
+apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
 done
@@ -256,7 +255,7 @@
 apply simp
 (* main case *)
 apply simp
-apply (tactic "safe_tac set_cs")
+apply auto
 
 (* a: act A; a: act B *)
 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
@@ -415,7 +414,7 @@
 apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
-apply (tactic "safe_tac set_cs")
+apply auto
 
 (* Case a:A, a:B *)
 apply (frule divide_Seq)
@@ -903,7 +902,7 @@
               Forall (%x. x:ext(A||B)) tr)"
 
 apply (simp (no_asm) add: traces_def has_trace_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 
 (* ==> *)
 (* There is a schedule of A *)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -52,7 +52,7 @@
 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
 apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (simp add: compositionality_tr)
 apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2")
 prefer 2
@@ -60,7 +60,7 @@
 apply (erule conjE)+
 (* rewrite with proven subgoal *)
 apply (simp add: externals_of_par)
-apply (tactic "safe_tac set_cs")
+apply auto
 
 (* 2 goals, the 3rd has been solved automatically *)
 (* 1: Filter A2 x : traces A2 *)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -15,7 +15,7 @@
   "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]  
           ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A"
 apply (simp add: schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (frule inp_is_act)
 apply (simp add: executions_def)
 apply (tactic {* pair_tac "ex" 1 *})
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -60,9 +60,9 @@
                    is_live_ref_map f (C,M) (A,L) |]
                 ==> live_implements (C,M) (A,L)"
 apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
   (* Traces coincide, Lemma 1 *)
   apply (tactic {* pair_tac "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
@@ -80,8 +80,6 @@
   apply (erule lemma_2 [THEN spec, THEN mp])
   apply (simp add: reachable.reachable_0)
 
- (* Liveness *)
-apply auto
 done
 
 end
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -183,12 +183,10 @@
 apply (unfold corresp_ex_def)
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
 (* cons case *)
-apply (tactic "safe_tac set_cs")
-apply (simp add: mk_traceConc)
+apply (auto simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
 apply assumption
 apply (erule_tac x = "y" in allE)
-apply simp
 apply (simp add: move_subprop4 split add: split_if)
 done
 
@@ -214,8 +212,7 @@
 apply (rule impI)
 apply (tactic {* Seq_Finite_induct_tac 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
-apply (tactic {* pair_tac "a" 1 *})
+apply (auto simp add: split_paired_all)
 done
 
 
@@ -235,7 +232,7 @@
 apply simp
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac t = "f y" in lemma_2_1)
 
 (* Finite *)
@@ -270,7 +267,7 @@
   apply (unfold traces_def)
 
   apply (simp (no_asm) add: has_trace_def2)
-  apply (tactic "safe_tac set_cs")
+  apply auto
 
   (* give execution of abstract automata *)
   apply (rule_tac x = "corresp_ex A f ex" in bexI)
@@ -322,9 +319,9 @@
           !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
           ==> fairtraces C <= fairtraces A"
 apply (simp (no_asm) add: fairtraces_def fairexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
 
   (* Traces coincide, Lemma 1 *)
   apply (tactic {* pair_tac "ex" 1 *})
@@ -342,8 +339,6 @@
   apply (erule lemma_2 [THEN spec, THEN mp])
   apply (simp add: reachable.reachable_0)
 
- (* Fairness *)
-apply auto
 done
 
 lemma fair_trace_inclusion2: "!! C A.
@@ -351,9 +346,10 @@
              is_fair_ref_map f C A |]
           ==> fair_implements C A"
 apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply (tactic "safe_tac set_cs")
+apply auto
+
   (* Traces coincide, Lemma 1 *)
   apply (tactic {* pair_tac "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
@@ -371,8 +367,6 @@
   apply (erule lemma_2 [THEN spec, THEN mp])
   apply (simp add: reachable.reachable_0)
 
- (* Fairness *)
-apply auto
 done
 
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -73,12 +73,9 @@
   "[| ext C = ext A;  
      is_weak_ref_map f C A |] ==> is_ref_map f C A"
 apply (unfold is_weak_ref_map_def is_ref_map_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (case_tac "a:ext A")
-apply (rule transition_is_ex)
-apply (simp (no_asm_simp))
-apply (rule nothing_is_ex)
-apply simp
+apply (auto intro: transition_is_ex nothing_is_ex)
 done
 
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -223,11 +223,11 @@
                LastActExtsch A sch"
 
 apply (unfold schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
 apply (simp add: executions_def)
 apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
 apply (simp (no_asm_simp))
 
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -174,14 +174,13 @@
 
 apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
 (* cons case *)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rename_tac ex a t s s')
 apply (simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
 apply assumption
 apply (erule_tac x = "t" in allE)
 apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
-apply simp
 apply (simp add: move_subprop5_sim [unfolded Let_def]
   move_subprop4_sim [unfolded Let_def] split add: split_if)
 done
@@ -200,7 +199,7 @@
 
 apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
 (* main case *)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (rename_tac ex a t s s')
 apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
 
@@ -262,7 +261,7 @@
   apply (unfold traces_def)
 
   apply (simp (no_asm) add: has_trace_def2)
-  apply (tactic "safe_tac set_cs")
+  apply auto
 
   (* give execution of abstract automata *)
   apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -166,7 +166,7 @@
               .--> (Next (Init (%(s,a,t).Q s))))"
 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
 
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
 apply (simp split add: split_if)
 (* TL = UU *)
 apply (rule conjI)
diff -r d6a508c16908 -r 6d437bde2f1d src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -345,21 +345,7 @@
 lemma has_trace_def2: 
 "has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
 apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
-(* 1 *)
-apply (rule_tac x = "ex" in bexI)
-apply (simplesubst beta_cfun)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-(* 2 *)
-apply (rule_tac x = "filter_act$ (snd ex) " in bexI)
-apply (simplesubst beta_cfun)
-apply (tactic "cont_tacR 1")
-apply (simp (no_asm))
-apply (tactic "safe_tac set_cs")
-apply (rule_tac x = "ex" in bexI)
-apply simp_all
+apply auto
 done
 
 
@@ -376,9 +362,7 @@
 apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
   thm "Forall_def", thm "sforall_def"] 1 *})
 (* main case *)
-apply (rename_tac ss a t)
-apply (tactic "safe_tac set_cs")
-apply (simp_all add: is_trans_of_def)
+apply (auto simp add: is_trans_of_def)
 done
 
 lemma exec_in_sig: