1.1 --- a/src/HOL/IMPP/Misc.ML	Tue Mar 28 12:28:24 2000 +0200
     1.2 +++ b/src/HOL/IMPP/Misc.ML	Tue Mar 28 17:31:36 2000 +0200
     1.3 @@ -13,8 +13,6 @@
     1.4  Goalw [update_def] "s[Loc Y::=s<Y>] = s";
     1.5  by (induct_tac "s" 1);
     1.6  by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
     1.7 -br ext 1;
     1.8 -by (Simp_tac 1);
     1.9  qed "update_Loc_idem2";
    1.10  Addsimps[update_Loc_idem2];
    1.11  

     2.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Tue Mar 28 12:28:24 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Tue Mar 28 17:31:36 2000 +0200
     2.3 @@ -33,10 +33,7 @@
     2.4  val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
     2.5  "\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
     2.6  	pair_tac "r" 1,
     2.7 -	Asm_full_simp_tac 1,
     2.8 -	strip_tac1 1,
     2.9 -	option_case_tac 1,
    2.10 -	Fast_tac 1]);
    2.11 +	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
    2.12  
    2.13  Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
    2.14  by(etac tranclE 1);

     3.1 --- a/src/HOL/ex/Factorization.ML	Tue Mar 28 12:28:24 2000 +0200
     3.2 +++ b/src/HOL/ex/Factorization.ML	Tue Mar 28 17:31:36 2000 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4  Goal "nondec xs --> nondec (oinsert x xs)";
     3.5  by (induct_tac "xs" 1);
     3.6  by (case_tac "list" 2);
     3.7 -by (ALLGOALS (Asm_full_simp_tac));
     3.8 +by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"])));
     3.9  qed_spec_mp "nondec_oinsert";
    3.10  
    3.11  Goal "nondec (sort xs)";

     4.1 --- a/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 12:28:24 2000 +0200
     4.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Tue Mar 28 17:31:36 2000 +0200
     4.3 @@ -22,9 +22,8 @@
     4.4  by (rtac imp_conj_lemma 1);
     4.5  by (simp_tac (simpset() addsimps [trans_of_def,
     4.6          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
     4.7 +by (induct_tac "a" 1);
     4.8  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
     4.9 -by (induct_tac "a" 1);
    4.10 -by Auto_tac;
    4.11  qed"h_abs_is_abstraction";
    4.12  
    4.13  

     5.1 --- a/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 12:28:24 2000 +0200
     5.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Tue Mar 28 17:31:36 2000 +0200
     5.3 @@ -22,9 +22,8 @@
     5.4  by (rtac imp_conj_lemma 1);
     5.5  by (simp_tac (simpset() addsimps [trans_of_def,
     5.6          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
     5.7 +by (induct_tac "a" 1);
     5.8  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
     5.9 -by (induct_tac "a" 1);
    5.10 -by Auto_tac;
    5.11  qed"h_abs_is_abstraction";
    5.12  
    5.13