1.1 --- a/src/HOL/Bali/Basis.thy	Mon Aug 01 20:21:11 2011 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Tue Aug 02 10:03:12 2011 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  section "misc"
     1.6  
     1.7 -declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
     1.8 -
     1.9  declare split_if_asm  [split] option.split [split] option.split_asm [split]
    1.10  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.11  declare if_weak_cong [cong del] option.weak_case_cong [cong del]

     2.1 --- a/src/HOL/ZF/Games.thy	Mon Aug 01 20:21:11 2011 +0200
     2.2 +++ b/src/HOL/ZF/Games.thy	Tue Aug 02 10:03:12 2011 +0200
     2.3 @@ -320,7 +320,7 @@
     2.4    apply (simp add: wfzf_is_option_of)
     2.5    done
     2.6  
     2.7 -lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
     2.8 +lemma wf_option_of[simp, intro]: "wf option_of"
     2.9  proof -
    2.10    have option_of: "option_of = inv_image is_option_of Rep_game"
    2.11      apply (rule set_eqI)

     3.1 --- a/src/HOL/ZF/LProd.thy	Mon Aug 01 20:21:11 2011 +0200
     3.2 +++ b/src/HOL/ZF/LProd.thy	Tue Aug 02 10:03:12 2011 +0200
     3.3 @@ -82,7 +82,7 @@
     3.4    qed
     3.5  qed
     3.6  
     3.7 -lemma wf_lprod[recdef_wf,simp,intro]:
     3.8 +lemma wf_lprod[simp,intro]:
     3.9    assumes wf_R: "wf R"
    3.10    shows "wf (lprod R)"
    3.11  proof -
    3.12 @@ -116,7 +116,7 @@
    3.13    by (auto intro: lprod_list[where a=c and b=c and 
    3.14      ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
    3.15  
    3.16 -lemma [recdef_wf, simp, intro]: 
    3.17 +lemma [simp, intro]:
    3.18    assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
    3.19  proof -
    3.20    have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
    3.21 @@ -125,7 +125,7 @@
    3.22      by (rule_tac wf_subset, auto)
    3.23  qed
    3.24  
    3.25 -lemma [recdef_wf, simp, intro]: 
    3.26 +lemma [simp, intro]:
    3.27    assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
    3.28  proof -
    3.29    have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"

     4.1 --- a/src/HOL/ZF/Zet.thy	Mon Aug 01 20:21:11 2011 +0200
     4.2 +++ b/src/HOL/ZF/Zet.thy	Tue Aug 02 10:03:12 2011 +0200
     4.3 @@ -196,7 +196,7 @@
     4.4  lemma zimage_id[simp]: "zimage id A = A"
     4.5    by (simp add: zet_ext_eq zimage_iff)
     4.6  
     4.7 -lemma zimage_cong[recdef_cong, fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
     4.8 +lemma zimage_cong[fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
     4.9    by (auto simp add: zet_ext_eq zimage_iff)
    4.10  
    4.11  end