Adapted to new simplifier.
authorberghofe
Mon Sep 30 16:14:02 2002 +0200 (2002-09-30)
changeset 13601fd3e3d6b37b2
parent 13600 9702c8636a7b
child 13602 4cecd1e0f4a9
Adapted to new simplifier.
src/HOL/Algebra/poly/LongDiv.ML
src/HOL/Auth/Guard/Guard_Shared.thy
src/HOL/Auth/Guard/Proto.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Divides_lemmas.ML
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/OG_Hoare.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/HoareParallel/RG_Tran.thy
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/NthRoot.ML
src/HOL/Hyperreal/Poly.ML
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/IntDiv.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
src/HOL/MiniML/W.ML
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Power.ML
src/HOL/Real/PReal.ML
src/HOL/TLA/Buffer/Buffer.ML
src/HOL/TLA/Buffer/DBuffer.ML
src/HOL/TLA/Memory/MemoryImplementation.ML
src/HOL/UNITY/Constrains.ML
src/HOL/UNITY/Simple/Lift.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/Unix/Unix.thy
src/HOL/W0/W0.thy
src/HOL/ex/AVL.ML
src/HOLCF/Sprod0.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOL/Algebra/poly/LongDiv.ML	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  by (Asm_simp_tac 1);
     1.5  (* proof of 1 *)
     1.6  by (rtac diff_zero_imp_eq 1);
     1.7 -by (Asm_full_simp_tac 1);
     1.8 +by (hyp_subst_tac 1);
     1.9  by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
    1.10  by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
    1.11  qed "long_div_quo_unique";
     2.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Mon Sep 30 16:12:16 2002 +0200
     2.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Mon Sep 30 16:14:02 2002 +0200
     2.3 @@ -177,7 +177,7 @@
     2.4  lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
     2.5  shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
     2.6  apply (clarify, simp only: knows_decomp)
     2.7 -apply (drule GuardK_invKey_keyset, clarify, simp+, blast)
     2.8 +apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
     2.9  apply clarify
    2.10  apply (drule in_good, simp)
    2.11  apply (drule in_shrK_set, simp+, clarify)
     3.1 --- a/src/HOL/Auth/Guard/Proto.thy	Mon Sep 30 16:12:16 2002 +0200
     3.2 +++ b/src/HOL/Auth/Guard/Proto.thy	Mon Sep 30 16:14:02 2002 +0200
     3.3 @@ -196,8 +196,7 @@
     3.4  apply (clarify, rule_tac x=k in exI, simp add: newn_def)
     3.5  apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
     3.6  apply (drule ok_not_used, simp+)
     3.7 -apply (clarify, erule ok_is_Says, simp+)
     3.8 -by blast
     3.9 +by (clarify, erule ok_is_Says, simp+)
    3.10  
    3.11  lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
    3.12  Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
     4.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Sep 30 16:12:16 2002 +0200
     4.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Sep 30 16:14:02 2002 +0200
     4.3 @@ -90,7 +90,7 @@
     4.4  apply (subgoal_tac 
     4.5          "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
     4.6  apply  clarsimp
     4.7 -apply  (erule thin_rl)
     4.8 +apply  (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
     4.9  apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
    4.10  apply   (auto dest!: not_initedD elim!: 
    4.11                simp add: nyinitcls_def inited_def split add: split_if_asm)
    4.12 @@ -386,8 +386,6 @@
    4.13  apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
    4.14  apply  (fast dest: unique_eval)
    4.15  apply clarsimp
    4.16 -apply (erule thin_rl)
    4.17 -apply (erule thin_rl)
    4.18  apply (drule split_paired_All [THEN subst])
    4.19  apply (clarsimp elim!: state_not_single)
    4.20  done
    4.21 @@ -678,10 +676,8 @@
    4.22      apply  (fast intro: ax_derivs_asm)
    4.23      apply (rule MGF_nested_Methd)
    4.24      apply (rule ballI)
    4.25 -    apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, 
    4.26 -           erule_tac [4] spec)
    4.27 +    apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
    4.28      apply   fast
    4.29 -    apply  (erule Suc_leD)
    4.30      apply (drule finite_subset)
    4.31      apply (erule finite_imageI)
    4.32      apply auto
     5.1 --- a/src/HOL/Bali/AxSound.thy	Mon Sep 30 16:12:16 2002 +0200
     5.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Sep 30 16:14:02 2002 +0200
     5.3 @@ -102,8 +102,9 @@
     5.4  apply (drule triples_valid2_Suc)
     5.5  apply (erule (1) notE impE)
     5.6  apply (drule_tac x = na in spec)
     5.7 -apply (tactic {* auto_tac (claset() addSIs [thm "Methd_triple_valid2_SucI"],
     5.8 -   simpset() addsimps [ball_Un] addloop ("split_all_tac", split_all_tac)) *})
     5.9 +apply (rule Methd_triple_valid2_SucI)
    5.10 +apply (simp (no_asm_use) add: ball_Un)
    5.11 +apply auto
    5.12  done
    5.13  
    5.14  
    5.15 @@ -351,7 +352,7 @@
    5.16  apply (frule wf_ws_prog) 
    5.17  apply (frule ty_expr_is_type [THEN type_is_class, 
    5.18                                THEN accfield_declC_is_class])
    5.19 -apply (simp,simp,simp) 
    5.20 +apply (simp (no_asm_use), simp (no_asm_use), simp (no_asm_use))
    5.21  apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
    5.22  apply (tactic "ALLGOALS sound_valid2_tac")
    5.23  apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
     6.1 --- a/src/HOL/Bali/Decl.thy	Mon Sep 30 16:12:16 2002 +0200
     6.2 +++ b/src/HOL/Bali/Decl.thy	Mon Sep 30 16:14:02 2002 +0200
     6.3 @@ -81,7 +81,7 @@
     6.4      have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
     6.5        by (auto simp add: less_acc_def split add: acc_modi.split)
     6.6      with prems show ?thesis
     6.7 -      by  (auto simp add: le_acc_def)
     6.8 +      by (unfold le_acc_def) rules
     6.9    qed
    6.10    next
    6.11    show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
     7.1 --- a/src/HOL/Bali/Eval.thy	Mon Sep 30 16:12:16 2002 +0200
     7.2 +++ b/src/HOL/Bali/Eval.thy	Mon Sep 30 16:14:02 2002 +0200
     7.3 @@ -160,6 +160,7 @@
     7.4  defer 
     7.5  apply (case_tac "a' = Null")
     7.6  apply  simp_all
     7.7 +apply rules
     7.8  done
     7.9  
    7.10  constdefs
    7.11 @@ -1203,8 +1204,7 @@
    7.12  lemma unique_eval [rule_format (no_asm)]: 
    7.13    "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
    7.14  apply (case_tac "ws")
    7.15 -apply (simp only:)
    7.16 -apply (erule thin_rl)
    7.17 +apply hypsubst
    7.18  apply (erule eval_induct)
    7.19  apply (tactic {* ALLGOALS (EVERY'
    7.20        [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
     8.1 --- a/src/HOL/Bali/Evaln.thy	Mon Sep 30 16:12:16 2002 +0200
     8.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Sep 30 16:14:02 2002 +0200
     8.3 @@ -600,7 +600,7 @@
     8.4                   mode: "mode = invmode statM e" and
     8.5                      T: "T =Inl (resTy statM)" and
     8.6          eq_accC_accC': "accC=accC'"
     8.7 -      by (rule wt_elim_cases) auto
     8.8 +      by (rule wt_elim_cases) fastsimp+
     8.9      from conf_s0 wt_e hyp_e
    8.10      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
    8.11        by blast
    8.12 @@ -1558,7 +1558,7 @@
    8.13                   mode: "mode = invmode statM e" and
    8.14                      T: "T =Inl (resTy statM)" and
    8.15          eq_accC_accC': "accC=accC'"
    8.16 -      by (rule wt_elim_cases) auto
    8.17 +      by (rule wt_elim_cases) fastsimp+
    8.18      from conf_s0 wt_e
    8.19      obtain n1 where
    8.20        evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
    8.21 @@ -1793,7 +1793,7 @@
    8.22                  stat: "stat=is_static f" and
    8.23                 accC': "accC'=accC" and
    8.24  	           T: "T=(Inl (type f))"
    8.25 -       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
    8.26 +       by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
    8.27      from wf wt_e 
    8.28      have iscls_statC: "is_class G statC"
    8.29        by (auto dest: ty_expr_is_type type_is_class)
     9.1 --- a/src/HOL/Bali/Table.thy	Mon Sep 30 16:12:16 2002 +0200
     9.2 +++ b/src/HOL/Bali/Table.thy	Mon Sep 30 16:14:02 2002 +0200
     9.3 @@ -171,7 +171,7 @@
     9.4  "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
     9.5    \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
     9.6   \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
     9.7 -apply (auto simp add: filter_tab_def)
     9.8 +apply (force simp add: filter_tab_def)
     9.9  done
    9.10  
    9.11  lemma cond_override_filter: 
    10.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Sep 30 16:12:16 2002 +0200
    10.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Sep 30 16:14:02 2002 +0200
    10.3 @@ -1895,7 +1895,7 @@
    10.4                   mode: "mode = invmode statM e" and
    10.5                      T: "T =Inl (resTy statM)" and
    10.6          eq_accC_accC': "accC=accC'"
    10.7 -      by (rule wt_elim_cases) auto
    10.8 +      by (rule wt_elim_cases) fastsimp+
    10.9      from conf_s0 wt_e hyp_e 
   10.10      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
   10.11             conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
   10.12 @@ -1947,7 +1947,7 @@
   10.13  	by auto
   10.14        ultimately have
   10.15  	"set_lvars (locals (store s2)) s4 = s2"
   10.16 -	by (cases s2,cases s4) (simp add: init_lvars_def2)
   10.17 +	by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
   10.18        with False conf_s2 error_free_s2
   10.19        show ?thesis
   10.20  	by auto
   10.21 @@ -1981,7 +1981,7 @@
   10.22  	ultimately have
   10.23  	  "set_lvars (locals (store s2)) s4 
   10.24             = (Some (Xcpt (Std NullPointer)),store s2)"
   10.25 -	  by (cases s2,cases s4) (simp add: init_lvars_def2)
   10.26 +	  by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
   10.27  	with conf_s2 error_free_s2
   10.28  	show ?thesis
   10.29  	  by (cases s2) (auto dest: conforms_NormI)
    11.1 --- a/src/HOL/Bali/WellForm.thy	Mon Sep 30 16:12:16 2002 +0200
    11.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Sep 30 16:14:02 2002 +0200
    11.3 @@ -1420,10 +1420,10 @@
    11.4    show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
    11.5    proof (induct rule: ws_class_induct')  
    11.6      case Object
    11.7 -    with wf have declC: "declclass m = Object"
    11.8 -      by (blast intro: declclass_methd_Object)
    11.9 -    with Object wf have "G\<turnstile>Methd sig m declared_in Object"
   11.10 -      by (auto dest: methd_declaredD simp del: methd_Object)
   11.11 +    with wf have declC: "Object = declclass m"
   11.12 +      by (simp add: declclass_methd_Object)
   11.13 +    from Object wf have "G\<turnstile>Methd sig m declared_in Object"
   11.14 +      by (auto intro: methd_declaredD simp add: declC)
   11.15      with declC 
   11.16      show "?MemberOf Object"
   11.17        by (auto intro!: members.Immediate
   11.18 @@ -2794,7 +2794,7 @@
   11.19        proof -
   11.20  	from im statM statT isT_statT wf not_Private_statM 
   11.21  	have "is_static im = is_static statM"
   11.22 -	  by (auto dest: wf_imethds_hiding_objmethdsD)
   11.23 +	  by (fastsimp dest: wf_imethds_hiding_objmethdsD)
   11.24  	with wf isT_statT statT im 
   11.25  	have "\<not> is_static statM"
   11.26  	  by (auto dest: wf_prog_idecl imethds_wf_mhead)
    12.1 --- a/src/HOL/Divides_lemmas.ML	Mon Sep 30 16:12:16 2002 +0200
    12.2 +++ b/src/HOL/Divides_lemmas.ML	Mon Sep 30 16:14:02 2002 +0200
    12.3 @@ -269,8 +269,7 @@
    12.4  Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
    12.5  \     ==> q = q'";
    12.6  by (asm_full_simp_tac 
    12.7 -    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
    12.8 -by Auto_tac;  
    12.9 +    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);  
   12.10  by (REPEAT 
   12.11      (blast_tac (claset() addIs [order_antisym]
   12.12  			 addDs [order_eq_refl RS unique_quotient_lemma, 
    13.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Mon Sep 30 16:12:16 2002 +0200
    13.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Mon Sep 30 16:14:02 2002 +0200
    13.3 @@ -203,7 +203,7 @@
    13.4  apply simp
    13.5  apply(subgoal_tac "ind x = length (E x)")
    13.6   apply (rotate_tac -1)
    13.7 - apply simp
    13.8 + apply (simp (asm_lr))
    13.9   apply(drule Graph1)
   13.10     apply simp
   13.11    apply clarify  
   13.12 @@ -320,7 +320,7 @@
   13.13  apply simp
   13.14  apply(subgoal_tac "ind x = length (E x)")
   13.15   apply (rotate_tac -1)
   13.16 - apply simp
   13.17 + apply (simp (asm_lr))
   13.18   apply(drule Graph1)
   13.19     apply simp
   13.20    apply clarify  
   13.21 @@ -555,12 +555,6 @@
   13.22   apply (force simp add:BtoW_def)
   13.23  apply(erule Graph4)
   13.24     apply simp+
   13.25 -  apply (simp add:BtoW_def)
   13.26 -  apply force
   13.27 - apply (simp add:BtoW_def)
   13.28 - apply force
   13.29 -apply (simp add:BtoW_def)
   13.30 -apply force
   13.31  --{* 7 subgoals left *}
   13.32  apply(clarify, simp add:abbrev Graph6 Graph12)
   13.33  apply(erule conjE)+
   13.34 @@ -573,12 +567,6 @@
   13.35   apply (force simp add:BtoW_def)
   13.36  apply(erule Graph4)
   13.37     apply simp+
   13.38 -  apply (simp add:BtoW_def)
   13.39 -  apply force
   13.40 - apply (simp add:BtoW_def)
   13.41 - apply force
   13.42 -apply (simp add:BtoW_def)
   13.43 -apply force
   13.44  --{* 6 subgoals left *}
   13.45  apply(clarify, simp add:abbrev Graph6 Graph12)
   13.46  apply(erule conjE)+
   13.47 @@ -592,12 +580,6 @@
   13.48    apply (force simp add:BtoW_def)
   13.49   apply(erule Graph4)
   13.50      apply simp+
   13.51 -   apply (simp add:BtoW_def)
   13.52 -   apply force
   13.53 -  apply (simp add:BtoW_def)
   13.54 -  apply force
   13.55 - apply (simp add:BtoW_def)
   13.56 - apply force
   13.57  apply(simp add:BtoW_def nth_list_update) 
   13.58  apply force
   13.59  --{* 5 subgoals left *}
   13.60 @@ -614,12 +596,6 @@
   13.61    apply (force simp add:BtoW_def)
   13.62   apply(erule Graph4)
   13.63      apply simp+
   13.64 -   apply (simp add:BtoW_def)
   13.65 -   apply force
   13.66 -  apply (simp add:BtoW_def)
   13.67 -  apply force
   13.68 - apply (simp add:BtoW_def)
   13.69 - apply force
   13.70  apply(rule conjI)
   13.71   apply(simp add:nth_list_update)
   13.72   apply force
   13.73 @@ -646,14 +622,6 @@
   13.74   apply (force simp add:BtoW_def)
   13.75  apply(erule Graph4)
   13.76     apply simp+
   13.77 -  apply (simp add:BtoW_def)
   13.78 -  apply force
   13.79 - apply (simp add:BtoW_def)
   13.80 - apply force
   13.81 -apply (simp add:BtoW_def)
   13.82 -apply force
   13.83 ---{* 1 subgoal left *}
   13.84 -apply(simp add:abbrev)
   13.85  done
   13.86  
   13.87  lemma interfree_Redirect_Edge_Propagate_Black: 
    14.1 --- a/src/HOL/HoareParallel/Graph.thy	Mon Sep 30 16:12:16 2002 +0200
    14.2 +++ b/src/HOL/HoareParallel/Graph.thy	Mon Sep 30 16:14:02 2002 +0200
    14.3 @@ -56,7 +56,7 @@
    14.4  apply(case_tac "list")
    14.5   apply force
    14.6  apply simp
    14.7 -apply(rotate_tac -1)
    14.8 +apply(rotate_tac -2)
    14.9  apply(erule_tac x = "0" in all_dupE)
   14.10  apply simp
   14.11  apply clarify
   14.12 @@ -170,7 +170,6 @@
   14.13  apply(case_tac " length path - Suc 0 < m")
   14.14   apply(subgoal_tac "(length path - Suc m)=0")
   14.15    prefer 2 apply arith
   14.16 - apply(rotate_tac -1)
   14.17   apply(simp del: diff_is_0_eq)
   14.18   apply(subgoal_tac "Suc nata\<le>nat")
   14.19   prefer 2 apply arith
   14.20 @@ -188,7 +187,8 @@
   14.21   apply simp
   14.22   apply(case_tac "length path")
   14.23    apply force
   14.24 - apply simp
   14.25 +apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
   14.26 +apply simp
   14.27  apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
   14.28  apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
   14.29  apply simp
   14.30 @@ -303,11 +303,10 @@
   14.31   apply(case_tac "length path")
   14.32    apply force
   14.33   apply simp
   14.34 - apply(rotate_tac -5)
   14.35 - apply(erule_tac x = "nat" in allE)
   14.36 + apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
   14.37   apply simp
   14.38   apply clarify
   14.39 - apply(erule_tac x = "nat" in allE)
   14.40 + apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
   14.41   apply simp
   14.42   apply(case_tac "j<I")
   14.43    apply(erule_tac x = "j" in allE)
   14.44 @@ -344,11 +343,10 @@
   14.45   apply(case_tac "length path")
   14.46    apply force
   14.47   apply simp
   14.48 - apply(rotate_tac -5)
   14.49 - apply(erule_tac x = "nat" in allE)
   14.50 + apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
   14.51   apply simp
   14.52   apply clarify
   14.53 - apply(erule_tac x = "nat" in allE)
   14.54 + apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
   14.55   apply simp
   14.56   apply(case_tac "j\<le>R")
   14.57    apply(drule le_imp_less_or_eq)
    15.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Sep 30 16:12:16 2002 +0200
    15.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Sep 30 16:14:02 2002 +0200
    15.3 @@ -194,13 +194,13 @@
    15.4  --{* 6 subgoals left *}
    15.5  prefer 6
    15.6  apply(erule_tac x=i in allE)
    15.7 -apply force
    15.8 +apply fastsimp
    15.9  --{* 5 subgoals left *}
   15.10  prefer 5
   15.11  apply(tactic {* ALLGOALS (case_tac "j=k") *})
   15.12  --{* 10 subgoals left *}
   15.13  apply simp_all
   15.14 -apply(erule_tac x=i in allE)
   15.15 +apply(erule_tac x=k in allE)
   15.16  apply force
   15.17  --{* 9 subgoals left *}
   15.18  apply(case_tac "j=l")
   15.19 @@ -438,15 +438,15 @@
   15.20  --{* 112 subgoals left *}
   15.21  apply(simp_all (no_asm))
   15.22  apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
   15.23 ---{* 860 subgoals left *}
   15.24 +--{* 930 subgoals left *}
   15.25  apply(tactic {* ALLGOALS Clarify_tac *})
   15.26 -apply(simp_all only:length_0_conv [THEN sym])
   15.27 ---{* 36 subgoals left *}
   15.28 -apply (simp_all del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
   15.29 ---{* 32 subgoals left *}
   15.30 +apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
   15.31 +--{* 44 subgoals left *}
   15.32 +apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
   15.33 +--{* 33 subgoals left *}
   15.34  apply(tactic {* ALLGOALS Clarify_tac *})
   15.35  apply(tactic {* TRYALL arith_tac *})
   15.36 ---{* 9 subgoals left *}
   15.37 +--{* 10 subgoals left *}
   15.38  apply (force simp add:less_Suc_eq)
   15.39  apply(drule sym)
   15.40  apply (force simp add:less_Suc_eq)+
    16.1 --- a/src/HOL/HoareParallel/OG_Hoare.thy	Mon Sep 30 16:12:16 2002 +0200
    16.2 +++ b/src/HOL/HoareParallel/OG_Hoare.thy	Mon Sep 30 16:14:02 2002 +0200
    16.3 @@ -385,7 +385,6 @@
    16.4     apply(simp add:interfree_aux_def)
    16.5     apply clarify
    16.6     apply simp
    16.7 -   apply clarify
    16.8     apply(erule_tac x="pre y" in ballE)
    16.9      apply(force intro: converse_rtrancl_into_rtrancl 
   16.10            simp add: com_validity_def SEM_def sem_def All_None_def)
   16.11 @@ -408,7 +407,6 @@
   16.12  apply(simp add:interfree_aux_def)
   16.13  apply clarify
   16.14  apply simp
   16.15 -apply clarify
   16.16  apply(erule_tac x="pre y" in ballE)
   16.17   apply(force intro: converse_rtrancl_into_rtrancl 
   16.18         simp add: com_validity_def SEM_def sem_def All_None_def Help)
    17.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Sep 30 16:12:16 2002 +0200
    17.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon Sep 30 16:14:02 2002 +0200
    17.3 @@ -149,7 +149,7 @@
    17.4     apply simp
    17.5     apply(subgoal_tac "j=0")
    17.6      apply (rotate_tac -1)
    17.7 -    apply simp
    17.8 +    apply (simp (asm_lr))
    17.9     apply arith
   17.10    apply clarify
   17.11    apply(case_tac i,simp,simp)
   17.12 @@ -340,8 +340,6 @@
   17.13         apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
   17.14          apply assumption+
   17.15         apply simp+
   17.16 -     apply(erule_tac x=j in allE)
   17.17 -     apply force
   17.18      apply clarsimp
   17.19      apply fastsimp
   17.20  apply force+
    18.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Sep 30 16:12:16 2002 +0200
    18.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Sep 30 16:14:02 2002 +0200
    18.3 @@ -673,7 +673,7 @@
    18.4      apply(case_tac xsa,simp,simp)
    18.5      apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
    18.6      apply(rule conjI,erule CptnEnv)
    18.7 -    apply(simp add:lift_def)
    18.8 +    apply(simp (no_asm_use) add:lift_def)
    18.9     apply clarify
   18.10     apply(erule_tac x="Suc i" in allE, simp)
   18.11    apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran")
   18.12 @@ -706,7 +706,7 @@
   18.13   apply(case_tac xsa,simp,simp)
   18.14   apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
   18.15   apply(rule conjI,erule CptnEnv)
   18.16 - apply(simp add:lift_def)
   18.17 + apply(simp (no_asm_use) add:lift_def)
   18.18   apply(rule_tac x=ys in exI,simp)
   18.19  apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran")
   18.20   apply simp
   18.21 @@ -1238,22 +1238,18 @@
   18.22   apply clarify
   18.23   apply(case_tac "i=ib",simp)
   18.24    apply(erule etran.elims,simp)
   18.25 - apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
   18.26 + apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
   18.27 + apply (erule etran.elims)
   18.28   apply(case_tac "ia=m",simp)
   18.29 -  apply(erule etran.elims,simp)
   18.30 + apply simp
   18.31   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
   18.32   apply(subgoal_tac "ia<m",simp)
   18.33    prefer 2
   18.34    apply arith
   18.35   apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp)
   18.36   apply(simp add:same_state_def)
   18.37 - apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
   18.38 + apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
   18.39   apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
   18.40 - apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
   18.41 - apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
   18.42 - apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.43 - apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.44 - apply simp
   18.45  --{* or an e-tran in @{text "\<sigma>"}, 
   18.46  therefore it satisfies @{text "rely \<or> guar_{ib}"} *}
   18.47  apply (force simp add:par_assum_def same_state_def)
   18.48 @@ -1285,13 +1281,8 @@
   18.49  apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE)
   18.50  apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
   18.51  apply(simp add:same_state_def)
   18.52 -apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp)
   18.53 +apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE)
   18.54  apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp)
   18.55 -apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
   18.56 -apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
   18.57 -apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.58 -apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   18.59 -apply simp
   18.60  done
   18.61  
   18.62  lemma four: 
   18.63 @@ -1377,11 +1368,11 @@
   18.64   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
   18.65   apply(subgoal_tac "length x - 1 < length x",simp)
   18.66    apply(case_tac "x\<noteq>[]")
   18.67 -   apply(drule last_length2,simp)
   18.68 +   apply(simp add: last_length2)
   18.69     apply(erule_tac x="clist!i" in ballE)
   18.70      apply(simp add:same_state_def)
   18.71      apply(subgoal_tac "clist!i\<noteq>[]")
   18.72 -     apply(drule_tac xs="clist!i" in last_length2,simp)
   18.73 +     apply(simp add: last_length2)
   18.74      apply(case_tac x)
   18.75       apply (force simp add:par_cp_def)
   18.76      apply (force simp add:par_cp_def)
   18.77 @@ -1405,9 +1396,7 @@
   18.78   apply simp
   18.79  apply clarify
   18.80  apply(erule_tac x=ia in all_dupE)
   18.81 -apply simp
   18.82 -apply(rule subsetD)
   18.83 - apply simp
   18.84 +apply(rule subsetD, erule mp, assumption)
   18.85  apply(erule_tac pre=pre and rely=rely and x=x and s=s in  three)
   18.86   apply(erule_tac x=ic in allE,erule mp)
   18.87   apply simp_all
    19.1 --- a/src/HOL/HoareParallel/RG_Tran.thy	Mon Sep 30 16:12:16 2002 +0200
    19.2 +++ b/src/HOL/HoareParallel/RG_Tran.thy	Mon Sep 30 16:14:02 2002 +0200
    19.3 @@ -831,7 +831,7 @@
    19.4  apply(rule conjI)
    19.5   apply(simp add:same_state_def)
    19.6   apply clarify
    19.7 - apply(case_tac j,simp,simp)
    19.8 + apply(case_tac j, simp, simp (no_asm_simp))
    19.9   apply(case_tac "i=ia",simp,simp)
   19.10  apply(rule conjI)
   19.11   apply(simp add:same_program_def)
   19.12 @@ -862,7 +862,6 @@
   19.13   apply(rule_tac x=ia in exI,simp)
   19.14   apply(rule conjI)
   19.15    apply(case_tac "i=ia",simp,simp)
   19.16 -  apply(rotate_tac -1,simp)
   19.17   apply clarify
   19.18   apply(case_tac "i=l",simp)
   19.19    apply(case_tac "l=ia",simp,simp)
   19.20 @@ -871,8 +870,7 @@
   19.21   apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
   19.22  apply clarify
   19.23  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption)
   19.24 -apply(case_tac "i=ia",simp)
   19.25 -apply(rotate_tac -1,simp)
   19.26 +apply(case_tac "i=ia",simp,simp)
   19.27  done
   19.28  
   19.29  lemma one_iff_aux: "xs\<noteq>[] \<Longrightarrow> (\<forall>ys. ((xs, s)#ys \<in> par_cptn) = 
    20.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Sep 30 16:12:16 2002 +0200
    20.2 +++ b/src/HOL/Hyperreal/Lim.ML	Mon Sep 30 16:14:02 2002 +0200
    20.3 @@ -1644,7 +1644,6 @@
    20.4      lemma_BOLZANO2 1);
    20.5  by Safe_tac;
    20.6  by (ALLGOALS(Asm_full_simp_tac));
    20.7 -by (Blast_tac 2);
    20.8  by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
    20.9  by (rtac ccontr 1);
   20.10  by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
   20.11 @@ -1899,7 +1898,8 @@
   20.12      (simpset() addsimps [real_abs_def, real_inverse_eq_divide, 
   20.13                           pos_real_less_divide_eq,
   20.14                           symmetric real_diff_def]
   20.15 -               addsplits [split_if_asm]) 1);
   20.16 +               addsplits [split_if_asm]
   20.17 +               delsimprocs [fast_real_arith_simproc]) 1);
   20.18  by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
   20.19  by (arith_tac 2);
   20.20  by (asm_full_simp_tac
   20.21 @@ -2020,7 +2020,7 @@
   20.22  by (dres_inst_tac [("z","xa"),("w","b")] real_le_anti_sym 5);
   20.23  by (REPEAT(Asm_full_simp_tac 2));
   20.24  by (dtac real_dense 1 THEN etac exE 1);
   20.25 -by (res_inst_tac [("x","r")] exI 1 THEN Asm_full_simp_tac 1);
   20.26 +by (res_inst_tac [("x","r")] exI 1 THEN Asm_simp_tac 1);
   20.27  by (etac conjE 1);
   20.28  by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
   20.29  by (EVERY1[assume_tac, etac exE]);
   20.30 @@ -2157,7 +2157,7 @@
   20.31  Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
   20.32  \     ==> v((a + b)/2) = (v a + v b)/2";
   20.33  by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
   20.34 -by Auto_tac;
   20.35 +by Safe_tac;
   20.36  by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
   20.37  by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
   20.38  by (dtac real_less_half_sum 1);
    21.1 --- a/src/HOL/Hyperreal/NthRoot.ML	Mon Sep 30 16:12:16 2002 +0200
    21.2 +++ b/src/HOL/Hyperreal/NthRoot.ML	Mon Sep 30 16:14:02 2002 +0200
    21.3 @@ -30,7 +30,8 @@
    21.4  by (dtac not_real_leE 2);
    21.5  by (res_inst_tac [("x","1")] exI 2);
    21.6  by (ALLGOALS(rtac (setleI RS isUbI)));
    21.7 -by (Auto_tac);
    21.8 +by Safe_tac;
    21.9 +by (ALLGOALS Simp_tac);
   21.10  by (ALLGOALS(rtac ccontr));
   21.11  by (ALLGOALS(dtac not_real_leE));
   21.12  by (dtac realpow_ge_self2 1 THEN assume_tac 1);
    22.1 --- a/src/HOL/Hyperreal/Poly.ML	Mon Sep 30 16:12:16 2002 +0200
    22.2 +++ b/src/HOL/Hyperreal/Poly.ML	Mon Sep 30 16:14:02 2002 +0200
    22.3 @@ -1041,8 +1041,6 @@
    22.4  by (blast_tac (claset() addIs [order_poly]) 2);
    22.5  by (rtac order_mult 2);
    22.6  by (rtac notI 2 THEN Asm_full_simp_tac 2);
    22.7 -by (dres_inst_tac [("p","p")] pderiv_zero 2);
    22.8 -by (Asm_full_simp_tac 2);
    22.9  by (case_tac "order a p = 0" 1);
   22.10  by (Asm_full_simp_tac 1);
   22.11  by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1);
    23.1 --- a/src/HOL/Hyperreal/Transcendental.ML	Mon Sep 30 16:12:16 2002 +0200
    23.2 +++ b/src/HOL/Hyperreal/Transcendental.ML	Mon Sep 30 16:14:02 2002 +0200
    23.3 @@ -1132,7 +1132,7 @@
    23.4  qed "ln_mult";
    23.5  
    23.6  Goal "[| 0 < x; 0 < y |] ==> (ln x = ln y) = (x = y)";
    23.7 -by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2)],simpset()));
    23.8 +by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2 RS sym)],simpset()));
    23.9  qed "ln_inj_iff";
   23.10  Addsimps [ln_inj_iff];
   23.11  
    24.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Sep 30 16:12:16 2002 +0200
    24.2 +++ b/src/HOL/Integ/IntDiv.thy	Mon Sep 30 16:14:02 2002 +0200
    24.3 @@ -365,10 +365,10 @@
    24.4  
    24.5  lemma self_quotient: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> q = 1"
    24.6  apply (simp add: split_ifs quorem_def linorder_neq_iff)
    24.7 -apply (rule order_antisym, auto)
    24.8 +apply (rule order_antisym, safe, simp_all (no_asm_use))
    24.9  apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
   24.10  apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
   24.11 -apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
   24.12 +apply (force intro: self_quotient_aux1 self_quotient_aux2 simp only: zadd_commute zmult_zminus)+
   24.13  done
   24.14  
   24.15  lemma self_remainder: "[| quorem((a,a),(q,r));  a ~= (0::int) |] ==> r = 0"
    25.1 --- a/src/HOL/Lambda/ListOrder.thy	Mon Sep 30 16:12:16 2002 +0200
    25.2 +++ b/src/HOL/Lambda/ListOrder.thy	Mon Sep 30 16:14:02 2002 +0200
    25.3 @@ -48,7 +48,7 @@
    25.4     apply (erule exE)
    25.5     apply (rename_tac ts)
    25.6     apply (case_tac ts)
    25.7 -    apply force
    25.8 +    apply fastsimp
    25.9     apply force
   25.10    apply (erule disjE)
   25.11     apply blast
    26.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 30 16:12:16 2002 +0200
    26.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Sep 30 16:14:02 2002 +0200
    26.3 @@ -26,7 +26,6 @@
    26.4    by (Blast_tac 1);
    26.5   by (Clarify_tac 1);
    26.6   by (subgoal_tac "xs=[]" 1);
    26.7 -  by (rotate_tac ~1 1);
    26.8    by (Asm_full_simp_tac 1);
    26.9   by (Blast_tac 1);
   26.10  by (blast_tac (claset() addDs [in_set_butlastD]) 1);
    27.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 30 16:12:16 2002 +0200
    27.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 16:14:02 2002 +0200
    27.3 @@ -274,7 +274,8 @@
    27.4    apply (rule conjI)
    27.5     apply force
    27.6    apply safe
    27.7 -  apply (simp_all add: eq_sym_conv)
    27.8 +  apply simp_all
    27.9 +  apply (simp add: eq_sym_conv)
   27.10    done
   27.11  
   27.12  (*
    28.1 --- a/src/HOL/List.thy	Mon Sep 30 16:12:16 2002 +0200
    28.2 +++ b/src/HOL/List.thy	Mon Sep 30 16:14:02 2002 +0200
    28.3 @@ -1268,10 +1268,9 @@
    28.4   apply simp
    28.5   apply blast
    28.6  apply (simp add: image_Collect lex_prod_def)
    28.7 -apply auto
    28.8 +apply safe
    28.9  apply blast
   28.10 - apply (rename_tac a xys x xs' y ys')
   28.11 - apply (rule_tac x = "a # xys" in exI)
   28.12 + apply (rule_tac x = "ab # xys" in exI)
   28.13   apply simp
   28.14  apply (case_tac xys)
   28.15   apply simp_all
    29.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Mon Sep 30 16:12:16 2002 +0200
    29.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Mon Sep 30 16:14:02 2002 +0200
    29.3 @@ -353,18 +353,18 @@
    29.4      obtain a X ST where
    29.5        s1: "s1 = (a @ X # ST, b1)" and
    29.6        l:  "length a = length list"
    29.7 -      by (simp, elim exE conjE, simp)
    29.8 +      by (simp, elim exE conjE, simp (no_asm_simp))
    29.9  
   29.10      from Invoke s app2
   29.11      obtain a' X' ST' where
   29.12        s2: "s2 = (a' @ X' # ST', b2)" and
   29.13        l': "length a' = length list"
   29.14 -      by (simp, elim exE conjE, simp)
   29.15 +      by (simp, elim exE conjE, simp (no_asm_simp))
   29.16  
   29.17      from l l'
   29.18      have lr: "length a = length a'" by simp
   29.19        
   29.20 -    from lr G s s1 s2 
   29.21 +    from lr G s1 s2 
   29.22      have "G \<turnstile> (ST, b1) <=s (ST', b2)"
   29.23        by (simp add: sup_state_append_fst sup_state_Cons1)
   29.24      
    30.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 30 16:12:16 2002 +0200
    30.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 30 16:14:02 2002 +0200
    30.3 @@ -136,12 +136,9 @@
    30.4         apply (blast dest: boundedD)
    30.5        apply blast
    30.6     apply clarify
    30.7 -   apply (rotate_tac -2)
    30.8     apply (erule allE)
    30.9     apply (erule impE)
   30.10      apply assumption
   30.11 -   apply (erule impE)
   30.12 -    apply assumption
   30.13     apply (drule bspec)
   30.14      apply assumption
   30.15     apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
   30.16 @@ -435,7 +432,6 @@
   30.17  defer
   30.18  apply assumption
   30.19  apply clarsimp
   30.20 -apply (blast dest!: boundedD)
   30.21  done
   30.22  
   30.23  
    31.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Mon Sep 30 16:12:16 2002 +0200
    31.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Mon Sep 30 16:14:02 2002 +0200
    31.3 @@ -215,7 +215,7 @@
    31.4      ck_types:   "check_types G mxs ?mxr ?phi" and
    31.5      wt_start:   "wt_start G C pTs mxl phi" and
    31.6      app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
    31.7 -    by (simp add: wt_method_def2)
    31.8 +    by (simp (asm_lr) add: wt_method_def2)
    31.9    
   31.10    have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
   31.11    hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
    32.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Mon Sep 30 16:12:16 2002 +0200
    32.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Sep 30 16:14:02 2002 +0200
    32.3 @@ -481,7 +481,6 @@
    32.4  apply clarify
    32.5  apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
    32.6   apply (blast dest: lift2_eq_ErrD)
    32.7 -apply blast
    32.8  done 
    32.9  
   32.10  lemma closed_err_lift2_conv:
    33.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 30 16:12:16 2002 +0200
    33.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 30 16:14:02 2002 +0200
    33.3 @@ -122,20 +122,14 @@
    33.4    apply clarsimp
    33.5    apply (rule_tac x="n'+2" in exI)  
    33.6    apply simp
    33.7 -  apply (drule listE_length)+
    33.8 -  apply fastsimp
    33.9  
   33.10    apply clarsimp
   33.11    apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
   33.12    apply simp
   33.13 -  apply (drule listE_length)+
   33.14 -  apply fastsimp
   33.15  
   33.16    apply clarsimp
   33.17    apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
   33.18    apply simp
   33.19 -  apply (drule listE_length)+
   33.20 -  apply fastsimp
   33.21  
   33.22    apply fastsimp
   33.23    apply fastsimp
    34.1 --- a/src/HOL/MiniML/W.ML	Mon Sep 30 16:12:16 2002 +0200
    34.2 +++ b/src/HOL/MiniML/W.ML	Mon Sep 30 16:14:02 2002 +0200
    34.3 @@ -473,7 +473,7 @@
    34.4  by (Fast_tac 3);
    34.5  (* case na : free_tv t - free_tv Sa *)
    34.6  by (Asm_full_simp_tac 2);
    34.7 -by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
    34.8 +by (dres_inst_tac [("A1", "$ S A"), ("r", "$ R ($ S A)")] (subst_comp_scheme_list RSN (2,trans)) 2);
    34.9  by (dtac eq_subst_scheme_list_eq_free 2);
   34.10  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   34.11  (** LEVEL 73 **)
    35.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Sep 30 16:12:16 2002 +0200
    35.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Sep 30 16:14:02 2002 +0200
    35.3 @@ -544,7 +544,6 @@
    35.4       apply (simp add: zgcd_commute)
    35.5      apply (simp add: zmult_commute)
    35.6     apply (auto simp add: dvd_def)
    35.7 -  apply (blast intro: sym)
    35.8    done
    35.9  
   35.10  lemma zcong_zless_imp_eq:
    36.1 --- a/src/HOL/Power.ML	Mon Sep 30 16:12:16 2002 +0200
    36.2 +++ b/src/HOL/Power.ML	Mon Sep 30 16:14:02 2002 +0200
    36.3 @@ -40,6 +40,7 @@
    36.4  by (induct_tac "n" 1);
    36.5  by Auto_tac;
    36.6  by (ALLGOALS (case_tac "m"));
    36.7 +by (Simp_tac 1);
    36.8  by Auto_tac;
    36.9  qed_spec_mp "power_inject";
   36.10  Addsimps [power_inject];
    37.1 --- a/src/HOL/Real/PReal.ML	Mon Sep 30 16:12:16 2002 +0200
    37.2 +++ b/src/HOL/Real/PReal.ML	Mon Sep 30 16:14:02 2002 +0200
    37.3 @@ -145,7 +145,7 @@
    37.4  
    37.5  Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
    37.6  by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
    37.7 -by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
    37.8 +by (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1);
    37.9  qed "not_in_preal_ub";
   37.10  
   37.11  (* preal_less is a strong order i.e nonreflexive and transitive *)
    38.1 --- a/src/HOL/TLA/Buffer/Buffer.ML	Mon Sep 30 16:12:16 2002 +0200
    38.2 +++ b/src/HOL/TLA/Buffer/Buffer.ML	Mon Sep 30 16:14:02 2002 +0200
    38.3 @@ -19,8 +19,8 @@
    38.4  (* ---------------------------- Action lemmas ---------------------------- *)
    38.5  
    38.6  (* Dequeue is visible *)
    38.7 -Goal "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
    38.8 -by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def]));
    38.9 +Goalw [angle_def,Deq_def] "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
   38.10 +by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
   38.11  qed "Deq_visible";
   38.12  
   38.13  (* Enabling condition for dequeue -- NOT NEEDED *)
    39.1 --- a/src/HOL/TLA/Buffer/DBuffer.ML	Mon Sep 30 16:12:16 2002 +0200
    39.2 +++ b/src/HOL/TLA/Buffer/DBuffer.ML	Mon Sep 30 16:14:02 2002 +0200
    39.3 @@ -31,8 +31,8 @@
    39.4  (*** Simulation of fairness ***)
    39.5  
    39.6  (* Compute enabledness predicates for DBDeq and DBPass actions *)
    39.7 -Goal "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq";
    39.8 -by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def]));
    39.9 +Goalw [angle_def,DBDeq_def,Deq_def] "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq";
   39.10 +by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
   39.11  qed "DBDeq_visible";
   39.12  
   39.13  Goalw [action_rewrite DBDeq_visible]
    40.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Mon Sep 30 16:12:16 2002 +0200
    40.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Mon Sep 30 16:14:02 2002 +0200
    40.3 @@ -738,7 +738,7 @@
    40.4  \        sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] \
    40.5  \     ==> sigma |= []<>S1 rmhist p";
    40.6  by (rtac classical 1);
    40.7 -by (asm_full_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1);
    40.8 +by (asm_lr_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1);
    40.9  by (auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [DBImplBD]));
   40.10  qed "S1Infinite";
   40.11  
    41.1 --- a/src/HOL/UNITY/Constrains.ML	Mon Sep 30 16:12:16 2002 +0200
    41.2 +++ b/src/HOL/UNITY/Constrains.ML	Mon Sep 30 16:14:02 2002 +0200
    41.3 @@ -399,7 +399,7 @@
    41.4  	      full_simp_tac (simpset() addsimps !program_defs_ref) 1,
    41.5  	      REPEAT (FIRSTGOAL (etac disjE)),
    41.6  	      ALLGOALS Clarify_tac,
    41.7 -	      ALLGOALS Asm_full_simp_tac]) i;
    41.8 +	      ALLGOALS Asm_lr_simp_tac]) i;
    41.9  
   41.10  
   41.11  (*For proving invariants*)
    42.1 --- a/src/HOL/UNITY/Simple/Lift.ML	Mon Sep 30 16:12:16 2002 +0200
    42.2 +++ b/src/HOL/UNITY/Simple/Lift.ML	Mon Sep 30 16:14:02 2002 +0200
    42.3 @@ -205,7 +205,7 @@
    42.4    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
    42.5  Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
    42.6  by (Clarify_tac 1);
    42.7 -by (auto_tac (claset(), metric_ss));
    42.8 +by (force_tac (claset(), metric_ss) 1);
    42.9  qed "E_thm16c";
   42.10  
   42.11  
    43.1 --- a/src/HOL/UNITY/SubstAx.ML	Mon Sep 30 16:12:16 2002 +0200
    43.2 +++ b/src/HOL/UNITY/SubstAx.ML	Mon Sep 30 16:14:02 2002 +0200
    43.3 @@ -436,4 +436,4 @@
    43.4  	      simp_tac (simpset() addsimps [Domain_def]) 3,
    43.5  	      constrains_tac 1,
    43.6  	      ALLGOALS Clarify_tac,
    43.7 -	      ALLGOALS Asm_full_simp_tac]);
    43.8 +	      ALLGOALS Asm_lr_simp_tac]);
    44.1 --- a/src/HOL/Unix/Unix.thy	Mon Sep 30 16:12:16 2002 +0200
    44.2 +++ b/src/HOL/Unix/Unix.thy	Mon Sep 30 16:14:02 2002 +0200
    44.3 @@ -464,7 +464,7 @@
    44.4      with root show ?thesis by cases auto
    44.5    next
    44.6      case readdir
    44.7 -    with root show ?thesis by cases auto
    44.8 +    with root show ?thesis by cases (simp (asm_lr))+
    44.9    qed
   44.10  qed
   44.11  
   44.12 @@ -1082,7 +1082,7 @@
   44.13              also have "\<dots> \<noteq> None"
   44.14              proof -
   44.15                from ys obtain us u where rev_ys: "ys = us @ [u]"
   44.16 -                by (cases ys rule: rev_cases) auto
   44.17 +                by (cases ys rule: rev_cases) fastsimp+
   44.18                with tr path
   44.19                have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
   44.20                    lookup root ((path @ [y]) @ us) \<noteq> None"
    45.1 --- a/src/HOL/W0/W0.thy	Mon Sep 30 16:12:16 2002 +0200
    45.2 +++ b/src/HOL/W0/W0.thy	Mon Sep 30 16:14:02 2002 +0200
    45.3 @@ -697,7 +697,7 @@
    45.4       apply (frule not_free_impl_id)
    45.5       apply simp
    45.6      txt {* @{text "na \<in> free_tv sa"} *}
    45.7 -    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
    45.8 +    apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
    45.9      apply (drule_tac eq_subst_tel_eq_free)
   45.10       apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   45.11      apply simp
   45.12 @@ -733,7 +733,7 @@
   45.13      defer
   45.14      txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
   45.15      apply simp
   45.16 -    apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
   45.17 +    apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
   45.18      apply (drule eq_subst_tel_eq_free)
   45.19       apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   45.20      apply (simp add: free_tv_subst dom_def)
   45.21 @@ -881,7 +881,7 @@
   45.22     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
   45.23    apply (erule (1) notE impE)
   45.24    apply (erule exE conjE)+
   45.25 -  apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   45.26 +  apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
   45.27    apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
   45.28     apply (simp add: new_tv_subst)
   45.29    apply (frule new_tv_subst_tel, assumption)
    46.1 --- a/src/HOL/ex/AVL.ML	Mon Sep 30 16:12:16 2002 +0200
    46.2 +++ b/src/HOL/ex/AVL.ML	Mon Sep 30 16:14:02 2002 +0200
    46.3 @@ -133,8 +133,7 @@
    46.4   by (fast_tac (claset() addss simpset()) 1);
    46.5  by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
    46.6   by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
    46.7 - by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
    46.8 - by (fast_tac (claset() addss simpset()) 1);
    46.9 + by (fast_tac (claset() addss (simpset() addsimps [max_def])) 1);
   46.10  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   46.11  by (fast_tac (claset() addss simpset()) 1);
   46.12  qed_spec_mp "height_insert";
    47.1 --- a/src/HOLCF/Sprod0.ML	Mon Sep 30 16:12:16 2002 +0200
    47.2 +++ b/src/HOLCF/Sprod0.ML	Mon Sep 30 16:14:02 2002 +0200
    47.3 @@ -298,6 +298,6 @@
    47.4  Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
    47.5  by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
    47.6  by (rotate_tac ~1 1);
    47.7 -by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
    47.8 +by (asm_lr_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
    47.9  by (Asm_simp_tac 1);
   47.10  qed "Sel_injective_Sprod";
    48.1 --- a/src/HOLCF/ex/Stream.ML	Mon Sep 30 16:12:16 2002 +0200
    48.2 +++ b/src/HOLCF/ex/Stream.ML	Mon Sep 30 16:14:02 2002 +0200
    48.3 @@ -423,7 +423,6 @@
    48.4  by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
    48.5                  [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
    48.6  by  (dtac sym 1);
    48.7 -by  (rotate_tac 2 2);
    48.8  by  Auto_tac;
    48.9  qed "slen_scons_eq";
   48.10