Adapted to new simplifier.
--- a/src/HOL/Algebra/poly/LongDiv.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML Mon Sep 30 16:14:02 2002 +0200
@@ -172,7 +172,7 @@
by (Asm_simp_tac 1);
(* proof of 1 *)
by (rtac diff_zero_imp_eq 1);
-by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1);
by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1);
qed "long_div_quo_unique";
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Mon Sep 30 16:14:02 2002 +0200
@@ -177,7 +177,7 @@
lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
apply (clarify, simp only: knows_decomp)
-apply (drule GuardK_invKey_keyset, clarify, simp+, blast)
+apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps)
apply clarify
apply (drule in_good, simp)
apply (drule in_shrK_set, simp+, clarify)
--- a/src/HOL/Auth/Guard/Proto.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy Mon Sep 30 16:14:02 2002 +0200
@@ -196,8 +196,7 @@
apply (clarify, rule_tac x=k in exI, simp add: newn_def)
apply (clarify, drule_tac Y="msg x" and s=s in apm_parts)
apply (drule ok_not_used, simp+)
-apply (clarify, erule ok_is_Says, simp+)
-by blast
+by (clarify, erule ok_is_Says, simp+)
lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs;
Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev"
--- a/src/HOL/Bali/AxCompl.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy Mon Sep 30 16:14:02 2002 +0200
@@ -90,7 +90,7 @@
apply (subgoal_tac
"nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
apply clarsimp
-apply (erule thin_rl)
+apply (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
apply (auto dest!: not_initedD elim!:
simp add: nyinitcls_def inited_def split add: split_if_asm)
@@ -386,8 +386,6 @@
apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
apply (fast dest: unique_eval)
apply clarsimp
-apply (erule thin_rl)
-apply (erule thin_rl)
apply (drule split_paired_All [THEN subst])
apply (clarsimp elim!: state_not_single)
done
@@ -678,10 +676,8 @@
apply (fast intro: ax_derivs_asm)
apply (rule MGF_nested_Methd)
apply (rule ballI)
- apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE,
- erule_tac [4] spec)
+ apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
apply fast
- apply (erule Suc_leD)
apply (drule finite_subset)
apply (erule finite_imageI)
apply auto
--- a/src/HOL/Bali/AxSound.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/AxSound.thy Mon Sep 30 16:14:02 2002 +0200
@@ -102,8 +102,9 @@
apply (drule triples_valid2_Suc)
apply (erule (1) notE impE)
apply (drule_tac x = na in spec)
-apply (tactic {* auto_tac (claset() addSIs [thm "Methd_triple_valid2_SucI"],
- simpset() addsimps [ball_Un] addloop ("split_all_tac", split_all_tac)) *})
+apply (rule Methd_triple_valid2_SucI)
+apply (simp (no_asm_use) add: ball_Un)
+apply auto
done
@@ -351,7 +352,7 @@
apply (frule wf_ws_prog)
apply (frule ty_expr_is_type [THEN type_is_class,
THEN accfield_declC_is_class])
-apply (simp,simp,simp)
+apply (simp (no_asm_use), simp (no_asm_use), simp (no_asm_use))
apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
apply (tactic "ALLGOALS sound_valid2_tac")
apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
--- a/src/HOL/Bali/Decl.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/Decl.thy Mon Sep 30 16:14:02 2002 +0200
@@ -81,7 +81,7 @@
have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
by (auto simp add: less_acc_def split add: acc_modi.split)
with prems show ?thesis
- by (auto simp add: le_acc_def)
+ by (unfold le_acc_def) rules
qed
next
show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
--- a/src/HOL/Bali/Eval.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Sep 30 16:14:02 2002 +0200
@@ -160,6 +160,7 @@
defer
apply (case_tac "a' = Null")
apply simp_all
+apply rules
done
constdefs
@@ -1203,8 +1204,7 @@
lemma unique_eval [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
apply (case_tac "ws")
-apply (simp only:)
-apply (erule thin_rl)
+apply hypsubst
apply (erule eval_induct)
apply (tactic {* ALLGOALS (EVERY'
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
--- a/src/HOL/Bali/Evaln.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Sep 30 16:14:02 2002 +0200
@@ -600,7 +600,7 @@
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) auto
+ by (rule wt_elim_cases) fastsimp+
from conf_s0 wt_e hyp_e
have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
by blast
@@ -1558,7 +1558,7 @@
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) auto
+ by (rule wt_elim_cases) fastsimp+
from conf_s0 wt_e
obtain n1 where
evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
@@ -1793,7 +1793,7 @@
stat: "stat=is_static f" and
accC': "accC'=accC" and
T: "T=(Inl (type f))"
- by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
+ by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
from wf wt_e
have iscls_statC: "is_class G statC"
by (auto dest: ty_expr_is_type type_is_class)
--- a/src/HOL/Bali/Table.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/Table.thy Mon Sep 30 16:14:02 2002 +0200
@@ -171,7 +171,7 @@
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b;
\<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
\<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
-apply (auto simp add: filter_tab_def)
+apply (force simp add: filter_tab_def)
done
lemma cond_override_filter:
--- a/src/HOL/Bali/TypeSafe.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Sep 30 16:14:02 2002 +0200
@@ -1895,7 +1895,7 @@
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) auto
+ by (rule wt_elim_cases) fastsimp+
from conf_s0 wt_e hyp_e
obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
@@ -1947,7 +1947,7 @@
by auto
ultimately have
"set_lvars (locals (store s2)) s4 = s2"
- by (cases s2,cases s4) (simp add: init_lvars_def2)
+ by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
with False conf_s2 error_free_s2
show ?thesis
by auto
@@ -1981,7 +1981,7 @@
ultimately have
"set_lvars (locals (store s2)) s4
= (Some (Xcpt (Std NullPointer)),store s2)"
- by (cases s2,cases s4) (simp add: init_lvars_def2)
+ by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
with conf_s2 error_free_s2
show ?thesis
by (cases s2) (auto dest: conforms_NormI)
--- a/src/HOL/Bali/WellForm.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Bali/WellForm.thy Mon Sep 30 16:14:02 2002 +0200
@@ -1420,10 +1420,10 @@
show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C"
proof (induct rule: ws_class_induct')
case Object
- with wf have declC: "declclass m = Object"
- by (blast intro: declclass_methd_Object)
- with Object wf have "G\<turnstile>Methd sig m declared_in Object"
- by (auto dest: methd_declaredD simp del: methd_Object)
+ with wf have declC: "Object = declclass m"
+ by (simp add: declclass_methd_Object)
+ from Object wf have "G\<turnstile>Methd sig m declared_in Object"
+ by (auto intro: methd_declaredD simp add: declC)
with declC
show "?MemberOf Object"
by (auto intro!: members.Immediate
@@ -2794,7 +2794,7 @@
proof -
from im statM statT isT_statT wf not_Private_statM
have "is_static im = is_static statM"
- by (auto dest: wf_imethds_hiding_objmethdsD)
+ by (fastsimp dest: wf_imethds_hiding_objmethdsD)
with wf isT_statT statT im
have "\<not> is_static statM"
by (auto dest: wf_prog_idecl imethds_wf_mhead)
--- a/src/HOL/Divides_lemmas.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Divides_lemmas.ML Mon Sep 30 16:14:02 2002 +0200
@@ -269,8 +269,7 @@
Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |] \
\ ==> q = q'";
by (asm_full_simp_tac
- (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
-by Auto_tac;
+ (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
by (REPEAT
(blast_tac (claset() addIs [order_antisym]
addDs [order_eq_refl RS unique_quotient_lemma,
--- a/src/HOL/HoareParallel/Gar_Coll.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Mon Sep 30 16:14:02 2002 +0200
@@ -203,7 +203,7 @@
apply simp
apply(subgoal_tac "ind x = length (E x)")
apply (rotate_tac -1)
- apply simp
+ apply (simp (asm_lr))
apply(drule Graph1)
apply simp
apply clarify
@@ -320,7 +320,7 @@
apply simp
apply(subgoal_tac "ind x = length (E x)")
apply (rotate_tac -1)
- apply simp
+ apply (simp (asm_lr))
apply(drule Graph1)
apply simp
apply clarify
@@ -555,12 +555,6 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
--{* 7 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
@@ -573,12 +567,6 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
--{* 6 subgoals left *}
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
@@ -592,12 +580,6 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
apply(simp add:BtoW_def nth_list_update)
apply force
--{* 5 subgoals left *}
@@ -614,12 +596,6 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
apply(rule conjI)
apply(simp add:nth_list_update)
apply force
@@ -646,14 +622,6 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
- apply (simp add:BtoW_def)
- apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
---{* 1 subgoal left *}
-apply(simp add:abbrev)
done
lemma interfree_Redirect_Edge_Propagate_Black:
--- a/src/HOL/HoareParallel/Graph.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Mon Sep 30 16:14:02 2002 +0200
@@ -56,7 +56,7 @@
apply(case_tac "list")
apply force
apply simp
-apply(rotate_tac -1)
+apply(rotate_tac -2)
apply(erule_tac x = "0" in all_dupE)
apply simp
apply clarify
@@ -170,7 +170,6 @@
apply(case_tac " length path - Suc 0 < m")
apply(subgoal_tac "(length path - Suc m)=0")
prefer 2 apply arith
- apply(rotate_tac -1)
apply(simp del: diff_is_0_eq)
apply(subgoal_tac "Suc nata\<le>nat")
prefer 2 apply arith
@@ -188,7 +187,8 @@
apply simp
apply(case_tac "length path")
apply force
- apply simp
+apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
+apply simp
apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
apply simp
@@ -303,11 +303,10 @@
apply(case_tac "length path")
apply force
apply simp
- apply(rotate_tac -5)
- apply(erule_tac x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
apply simp
apply clarify
- apply(erule_tac x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
apply simp
apply(case_tac "j<I")
apply(erule_tac x = "j" in allE)
@@ -344,11 +343,10 @@
apply(case_tac "length path")
apply force
apply simp
- apply(rotate_tac -5)
- apply(erule_tac x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE)
apply simp
apply clarify
- apply(erule_tac x = "nat" in allE)
+ apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
apply simp
apply(case_tac "j\<le>R")
apply(drule le_imp_less_or_eq)
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Mon Sep 30 16:14:02 2002 +0200
@@ -194,13 +194,13 @@
--{* 6 subgoals left *}
prefer 6
apply(erule_tac x=i in allE)
-apply force
+apply fastsimp
--{* 5 subgoals left *}
prefer 5
apply(tactic {* ALLGOALS (case_tac "j=k") *})
--{* 10 subgoals left *}
apply simp_all
-apply(erule_tac x=i in allE)
+apply(erule_tac x=k in allE)
apply force
--{* 9 subgoals left *}
apply(case_tac "j=l")
@@ -438,15 +438,15 @@
--{* 112 subgoals left *}
apply(simp_all (no_asm))
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
---{* 860 subgoals left *}
+--{* 930 subgoals left *}
apply(tactic {* ALLGOALS Clarify_tac *})
-apply(simp_all only:length_0_conv [THEN sym])
---{* 36 subgoals left *}
-apply (simp_all del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
---{* 32 subgoals left *}
+apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
+--{* 44 subgoals left *}
+apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
+--{* 33 subgoals left *}
apply(tactic {* ALLGOALS Clarify_tac *})
apply(tactic {* TRYALL arith_tac *})
---{* 9 subgoals left *}
+--{* 10 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)
apply (force simp add:less_Suc_eq)+
--- a/src/HOL/HoareParallel/OG_Hoare.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Hoare.thy Mon Sep 30 16:14:02 2002 +0200
@@ -385,7 +385,6 @@
apply(simp add:interfree_aux_def)
apply clarify
apply simp
- apply clarify
apply(erule_tac x="pre y" in ballE)
apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def)
@@ -408,7 +407,6 @@
apply(simp add:interfree_aux_def)
apply clarify
apply simp
-apply clarify
apply(erule_tac x="pre y" in ballE)
apply(force intro: converse_rtrancl_into_rtrancl
simp add: com_validity_def SEM_def sem_def All_None_def Help)
--- a/src/HOL/HoareParallel/RG_Examples.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Mon Sep 30 16:14:02 2002 +0200
@@ -149,7 +149,7 @@
apply simp
apply(subgoal_tac "j=0")
apply (rotate_tac -1)
- apply simp
+ apply (simp (asm_lr))
apply arith
apply clarify
apply(case_tac i,simp,simp)
@@ -340,8 +340,6 @@
apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
apply assumption+
apply simp+
- apply(erule_tac x=j in allE)
- apply force
apply clarsimp
apply fastsimp
apply force+
--- a/src/HOL/HoareParallel/RG_Hoare.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Mon Sep 30 16:14:02 2002 +0200
@@ -673,7 +673,7 @@
apply(case_tac xsa,simp,simp)
apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
apply(rule conjI,erule CptnEnv)
- apply(simp add:lift_def)
+ apply(simp (no_asm_use) add:lift_def)
apply clarify
apply(erule_tac x="Suc i" in allE, simp)
apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran")
@@ -706,7 +706,7 @@
apply(case_tac xsa,simp,simp)
apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp)
apply(rule conjI,erule CptnEnv)
- apply(simp add:lift_def)
+ apply(simp (no_asm_use) add:lift_def)
apply(rule_tac x=ys in exI,simp)
apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran")
apply simp
@@ -1238,22 +1238,18 @@
apply clarify
apply(case_tac "i=ib",simp)
apply(erule etran.elims,simp)
- apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp)
+ apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE)
+ apply (erule etran.elims)
apply(case_tac "ia=m",simp)
- apply(erule etran.elims,simp)
+ apply simp
apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE)
apply(subgoal_tac "ia<m",simp)
prefer 2
apply arith
apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp)
apply(simp add:same_state_def)
- 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)
+ 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)
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)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
- apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
- apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
- apply simp
--{* or an e-tran in @{text "\<sigma>"},
therefore it satisfies @{text "rely \<or> guar_{ib}"} *}
apply (force simp add:par_assum_def same_state_def)
@@ -1285,13 +1281,8 @@
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)
apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE)
apply(simp add:same_state_def)
-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)
+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)
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)
-apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
-apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE)
-apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
-apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
-apply simp
done
lemma four:
@@ -1377,11 +1368,11 @@
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE)
apply(subgoal_tac "length x - 1 < length x",simp)
apply(case_tac "x\<noteq>[]")
- apply(drule last_length2,simp)
+ apply(simp add: last_length2)
apply(erule_tac x="clist!i" in ballE)
apply(simp add:same_state_def)
apply(subgoal_tac "clist!i\<noteq>[]")
- apply(drule_tac xs="clist!i" in last_length2,simp)
+ apply(simp add: last_length2)
apply(case_tac x)
apply (force simp add:par_cp_def)
apply (force simp add:par_cp_def)
@@ -1405,9 +1396,7 @@
apply simp
apply clarify
apply(erule_tac x=ia in all_dupE)
-apply simp
-apply(rule subsetD)
- apply simp
+apply(rule subsetD, erule mp, assumption)
apply(erule_tac pre=pre and rely=rely and x=x and s=s in three)
apply(erule_tac x=ic in allE,erule mp)
apply simp_all
--- a/src/HOL/HoareParallel/RG_Tran.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Tran.thy Mon Sep 30 16:14:02 2002 +0200
@@ -831,7 +831,7 @@
apply(rule conjI)
apply(simp add:same_state_def)
apply clarify
- apply(case_tac j,simp,simp)
+ apply(case_tac j, simp, simp (no_asm_simp))
apply(case_tac "i=ia",simp,simp)
apply(rule conjI)
apply(simp add:same_program_def)
@@ -862,7 +862,6 @@
apply(rule_tac x=ia in exI,simp)
apply(rule conjI)
apply(case_tac "i=ia",simp,simp)
- apply(rotate_tac -1,simp)
apply clarify
apply(case_tac "i=l",simp)
apply(case_tac "l=ia",simp,simp)
@@ -871,8 +870,7 @@
apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
apply clarify
apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption)
-apply(case_tac "i=ia",simp)
-apply(rotate_tac -1,simp)
+apply(case_tac "i=ia",simp,simp)
done
lemma one_iff_aux: "xs\<noteq>[] \<Longrightarrow> (\<forall>ys. ((xs, s)#ys \<in> par_cptn) =
--- a/src/HOL/Hyperreal/Lim.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Mon Sep 30 16:14:02 2002 +0200
@@ -1644,7 +1644,6 @@
lemma_BOLZANO2 1);
by Safe_tac;
by (ALLGOALS(Asm_full_simp_tac));
-by (Blast_tac 2);
by (asm_full_simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
by (rtac ccontr 1);
by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
@@ -1899,7 +1898,8 @@
(simpset() addsimps [real_abs_def, real_inverse_eq_divide,
pos_real_less_divide_eq,
symmetric real_diff_def]
- addsplits [split_if_asm]) 1);
+ addsplits [split_if_asm]
+ delsimprocs [fast_real_arith_simproc]) 1);
by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
by (arith_tac 2);
by (asm_full_simp_tac
@@ -2020,7 +2020,7 @@
by (dres_inst_tac [("z","xa"),("w","b")] real_le_anti_sym 5);
by (REPEAT(Asm_full_simp_tac 2));
by (dtac real_dense 1 THEN etac exE 1);
-by (res_inst_tac [("x","r")] exI 1 THEN Asm_full_simp_tac 1);
+by (res_inst_tac [("x","r")] exI 1 THEN Asm_simp_tac 1);
by (etac conjE 1);
by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
by (EVERY1[assume_tac, etac exE]);
@@ -2157,7 +2157,7 @@
Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
\ ==> v((a + b)/2) = (v a + v b)/2";
by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
-by Auto_tac;
+by Safe_tac;
by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
by (dtac real_less_half_sum 1);
--- a/src/HOL/Hyperreal/NthRoot.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Hyperreal/NthRoot.ML Mon Sep 30 16:14:02 2002 +0200
@@ -30,7 +30,8 @@
by (dtac not_real_leE 2);
by (res_inst_tac [("x","1")] exI 2);
by (ALLGOALS(rtac (setleI RS isUbI)));
-by (Auto_tac);
+by Safe_tac;
+by (ALLGOALS Simp_tac);
by (ALLGOALS(rtac ccontr));
by (ALLGOALS(dtac not_real_leE));
by (dtac realpow_ge_self2 1 THEN assume_tac 1);
--- a/src/HOL/Hyperreal/Poly.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Hyperreal/Poly.ML Mon Sep 30 16:14:02 2002 +0200
@@ -1041,8 +1041,6 @@
by (blast_tac (claset() addIs [order_poly]) 2);
by (rtac order_mult 2);
by (rtac notI 2 THEN Asm_full_simp_tac 2);
-by (dres_inst_tac [("p","p")] pderiv_zero 2);
-by (Asm_full_simp_tac 2);
by (case_tac "order a p = 0" 1);
by (Asm_full_simp_tac 1);
by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1);
--- a/src/HOL/Hyperreal/Transcendental.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML Mon Sep 30 16:14:02 2002 +0200
@@ -1132,7 +1132,7 @@
qed "ln_mult";
Goal "[| 0 < x; 0 < y |] ==> (ln x = ln y) = (x = y)";
-by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2)],simpset()));
+by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2 RS sym)],simpset()));
qed "ln_inj_iff";
Addsimps [ln_inj_iff];
--- a/src/HOL/Integ/IntDiv.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Integ/IntDiv.thy Mon Sep 30 16:14:02 2002 +0200
@@ -365,10 +365,10 @@
lemma self_quotient: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> q = 1"
apply (simp add: split_ifs quorem_def linorder_neq_iff)
-apply (rule order_antisym, auto)
+apply (rule order_antisym, safe, simp_all (no_asm_use))
apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)
-apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: zadd_commute zmult_zminus)+
+apply (force intro: self_quotient_aux1 self_quotient_aux2 simp only: zadd_commute zmult_zminus)+
done
lemma self_remainder: "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> r = 0"
--- a/src/HOL/Lambda/ListOrder.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Mon Sep 30 16:14:02 2002 +0200
@@ -48,7 +48,7 @@
apply (erule exE)
apply (rename_tac ts)
apply (case_tac ts)
- apply force
+ apply fastsimp
apply force
apply (erule disjE)
apply blast
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML Mon Sep 30 16:14:02 2002 +0200
@@ -26,7 +26,6 @@
by (Blast_tac 1);
by (Clarify_tac 1);
by (subgoal_tac "xs=[]" 1);
- by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
by (blast_tac (claset() addDs [in_set_butlastD]) 1);
--- a/src/HOL/Library/Multiset.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 30 16:14:02 2002 +0200
@@ -274,7 +274,8 @@
apply (rule conjI)
apply force
apply safe
- apply (simp_all add: eq_sym_conv)
+ apply simp_all
+ apply (simp add: eq_sym_conv)
done
(*
--- a/src/HOL/List.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/List.thy Mon Sep 30 16:14:02 2002 +0200
@@ -1268,10 +1268,9 @@
apply simp
apply blast
apply (simp add: image_Collect lex_prod_def)
-apply auto
+apply safe
apply blast
- apply (rename_tac a xys x xs' y ys')
- apply (rule_tac x = "a # xys" in exI)
+ apply (rule_tac x = "ab # xys" in exI)
apply simp
apply (case_tac xys)
apply simp_all
--- a/src/HOL/MicroJava/BV/EffectMono.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Mon Sep 30 16:14:02 2002 +0200
@@ -353,18 +353,18 @@
obtain a X ST where
s1: "s1 = (a @ X # ST, b1)" and
l: "length a = length list"
- by (simp, elim exE conjE, simp)
+ by (simp, elim exE conjE, simp (no_asm_simp))
from Invoke s app2
obtain a' X' ST' where
s2: "s2 = (a' @ X' # ST', b2)" and
l': "length a' = length list"
- by (simp, elim exE conjE, simp)
+ by (simp, elim exE conjE, simp (no_asm_simp))
from l l'
have lr: "length a = length a'" by simp
- from lr G s s1 s2
+ from lr G s1 s2
have "G \<turnstile> (ST, b1) <=s (ST', b2)"
by (simp add: sup_state_append_fst sup_state_Cons1)
--- a/src/HOL/MicroJava/BV/Kildall.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Mon Sep 30 16:14:02 2002 +0200
@@ -136,12 +136,9 @@
apply (blast dest: boundedD)
apply blast
apply clarify
- apply (rotate_tac -2)
apply (erule allE)
apply (erule impE)
apply assumption
- apply (erule impE)
- apply assumption
apply (drule bspec)
apply assumption
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
@@ -435,7 +432,6 @@
defer
apply assumption
apply clarsimp
-apply (blast dest!: boundedD)
done
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Mon Sep 30 16:14:02 2002 +0200
@@ -215,7 +215,7 @@
ck_types: "check_types G mxs ?mxr ?phi" and
wt_start: "wt_start G C pTs mxl phi" and
app_eff: "wt_app_eff (sup_state_opt G) ?app ?eff phi"
- by (simp add: wt_method_def2)
+ by (simp (asm_lr) add: wt_method_def2)
have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
--- a/src/HOL/MicroJava/BV/Listn.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Mon Sep 30 16:14:02 2002 +0200
@@ -481,7 +481,6 @@
apply clarify
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
apply (blast dest: lift2_eq_ErrD)
-apply blast
done
lemma closed_err_lift2_conv:
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 30 16:14:02 2002 +0200
@@ -122,20 +122,14 @@
apply clarsimp
apply (rule_tac x="n'+2" in exI)
apply simp
- apply (drule listE_length)+
- apply fastsimp
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
apply simp
- apply (drule listE_length)+
- apply fastsimp
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
apply simp
- apply (drule listE_length)+
- apply fastsimp
apply fastsimp
apply fastsimp
--- a/src/HOL/MiniML/W.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MiniML/W.ML Mon Sep 30 16:14:02 2002 +0200
@@ -473,7 +473,7 @@
by (Fast_tac 3);
(* case na : free_tv t - free_tv Sa *)
by (Asm_full_simp_tac 2);
-by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
+by (dres_inst_tac [("A1", "$ S A"), ("r", "$ R ($ S A)")] (subst_comp_scheme_list RSN (2,trans)) 2);
by (dtac eq_subst_scheme_list_eq_free 2);
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
(** LEVEL 73 **)
--- a/src/HOL/NumberTheory/IntPrimes.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Sep 30 16:14:02 2002 +0200
@@ -544,7 +544,6 @@
apply (simp add: zgcd_commute)
apply (simp add: zmult_commute)
apply (auto simp add: dvd_def)
- apply (blast intro: sym)
done
lemma zcong_zless_imp_eq:
--- a/src/HOL/Power.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Power.ML Mon Sep 30 16:14:02 2002 +0200
@@ -40,6 +40,7 @@
by (induct_tac "n" 1);
by Auto_tac;
by (ALLGOALS (case_tac "m"));
+by (Simp_tac 1);
by Auto_tac;
qed_spec_mp "power_inject";
Addsimps [power_inject];
--- a/src/HOL/Real/PReal.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Real/PReal.ML Mon Sep 30 16:14:02 2002 +0200
@@ -145,7 +145,7 @@
Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
-by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
+by (fast_tac (claset() addIs [not_less_not_eq_prat_less] addss simpset()) 1);
qed "not_in_preal_ub";
(* preal_less is a strong order i.e nonreflexive and transitive *)
--- a/src/HOL/TLA/Buffer/Buffer.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.ML Mon Sep 30 16:14:02 2002 +0200
@@ -19,8 +19,8 @@
(* ---------------------------- Action lemmas ---------------------------- *)
(* Dequeue is visible *)
-Goal "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
-by (auto_tac (claset(), simpset() addsimps [angle_def,Deq_def]));
+Goalw [angle_def,Deq_def] "|- <Deq ic q oc>_(ic,q,oc) = Deq ic q oc";
+by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
qed "Deq_visible";
(* Enabling condition for dequeue -- NOT NEEDED *)
--- a/src/HOL/TLA/Buffer/DBuffer.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.ML Mon Sep 30 16:14:02 2002 +0200
@@ -31,8 +31,8 @@
(*** Simulation of fairness ***)
(* Compute enabledness predicates for DBDeq and DBPass actions *)
-Goal "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq";
-by (auto_tac (db_css addsimps2 [angle_def,DBDeq_def,Deq_def]));
+Goalw [angle_def,DBDeq_def,Deq_def] "|- <DBDeq>_(inp,mid,out,q1,q2) = DBDeq";
+by (REPEAT (Safe_tac THEN Asm_lr_simp_tac 1));
qed "DBDeq_visible";
Goalw [action_rewrite DBDeq_visible]
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Mon Sep 30 16:14:02 2002 +0200
@@ -738,7 +738,7 @@
\ sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] \
\ ==> sigma |= []<>S1 rmhist p";
by (rtac classical 1);
-by (asm_full_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1);
+by (asm_lr_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1);
by (auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [DBImplBD]));
qed "S1Infinite";
--- a/src/HOL/UNITY/Constrains.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/UNITY/Constrains.ML Mon Sep 30 16:14:02 2002 +0200
@@ -399,7 +399,7 @@
full_simp_tac (simpset() addsimps !program_defs_ref) 1,
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
- ALLGOALS Asm_full_simp_tac]) i;
+ ALLGOALS Asm_lr_simp_tac]) i;
(*For proving invariants*)
--- a/src/HOL/UNITY/Simple/Lift.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/UNITY/Simple/Lift.ML Mon Sep 30 16:14:02 2002 +0200
@@ -205,7 +205,7 @@
i.e. the trivial disjunction, leading to an asymmetrical proof.*)
Goal "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
by (Clarify_tac 1);
-by (auto_tac (claset(), metric_ss));
+by (force_tac (claset(), metric_ss) 1);
qed "E_thm16c";
--- a/src/HOL/UNITY/SubstAx.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Mon Sep 30 16:14:02 2002 +0200
@@ -436,4 +436,4 @@
simp_tac (simpset() addsimps [Domain_def]) 3,
constrains_tac 1,
ALLGOALS Clarify_tac,
- ALLGOALS Asm_full_simp_tac]);
+ ALLGOALS Asm_lr_simp_tac]);
--- a/src/HOL/Unix/Unix.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/Unix/Unix.thy Mon Sep 30 16:14:02 2002 +0200
@@ -464,7 +464,7 @@
with root show ?thesis by cases auto
next
case readdir
- with root show ?thesis by cases auto
+ with root show ?thesis by cases (simp (asm_lr))+
qed
qed
@@ -1082,7 +1082,7 @@
also have "\<dots> \<noteq> None"
proof -
from ys obtain us u where rev_ys: "ys = us @ [u]"
- by (cases ys rule: rev_cases) auto
+ by (cases ys rule: rev_cases) fastsimp+
with tr path
have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
lookup root ((path @ [y]) @ us) \<noteq> None"
--- a/src/HOL/W0/W0.thy Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/W0/W0.thy Mon Sep 30 16:14:02 2002 +0200
@@ -697,7 +697,7 @@
apply (frule not_free_impl_id)
apply simp
txt {* @{text "na \<in> free_tv sa"} *}
- apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
+ apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
apply (drule_tac eq_subst_tel_eq_free)
apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
apply simp
@@ -733,7 +733,7 @@
defer
txt {* case @{text "na \<in> free_tv t - free_tv sa"} *}
apply simp
- apply (drule_tac ts1 = "$s a" in subst_comp_tel [THEN [2] trans])
+ apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
apply (drule eq_subst_tel_eq_free)
apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
apply (simp add: free_tv_subst dom_def)
@@ -881,7 +881,7 @@
apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
apply (erule (1) notE impE)
apply (erule exE conjE)+
- apply (simp add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
+ apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra")
apply (simp add: new_tv_subst)
apply (frule new_tv_subst_tel, assumption)
--- a/src/HOL/ex/AVL.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/ex/AVL.ML Mon Sep 30 16:14:02 2002 +0200
@@ -133,8 +133,7 @@
by (fast_tac (claset() addss simpset()) 1);
by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
by (forw_inst_tac [("n","nat")] height_r_bal 1);
- by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
- by (fast_tac (claset() addss simpset()) 1);
+ by (fast_tac (claset() addss (simpset() addsimps [max_def])) 1);
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
by (fast_tac (claset() addss simpset()) 1);
qed_spec_mp "height_insert";
--- a/src/HOLCF/Sprod0.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOLCF/Sprod0.ML Mon Sep 30 16:14:02 2002 +0200
@@ -298,6 +298,6 @@
Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y";
by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1);
by (rotate_tac ~1 1);
-by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
+by (asm_lr_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1);
by (Asm_simp_tac 1);
qed "Sel_injective_Sprod";
--- a/src/HOLCF/ex/Stream.ML Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOLCF/ex/Stream.ML Mon Sep 30 16:14:02 2002 +0200
@@ -423,7 +423,6 @@
by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
[thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
by (dtac sym 1);
-by (rotate_tac 2 2);
by Auto_tac;
qed "slen_scons_eq";