--- a/src/HOL/Bali/Basis.thy Mon Aug 01 20:21:11 2011 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Aug 02 10:03:12 2011 +0200
@@ -8,8 +8,6 @@
section "misc"
-declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
-
declare split_if_asm [split] option.split [split] option.split_asm [split]
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
--- a/src/HOL/ZF/Games.thy Mon Aug 01 20:21:11 2011 +0200
+++ b/src/HOL/ZF/Games.thy Tue Aug 02 10:03:12 2011 +0200
@@ -320,7 +320,7 @@
apply (simp add: wfzf_is_option_of)
done
-lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
+lemma wf_option_of[simp, intro]: "wf option_of"
proof -
have option_of: "option_of = inv_image is_option_of Rep_game"
apply (rule set_eqI)
--- a/src/HOL/ZF/LProd.thy Mon Aug 01 20:21:11 2011 +0200
+++ b/src/HOL/ZF/LProd.thy Tue Aug 02 10:03:12 2011 +0200
@@ -82,7 +82,7 @@
qed
qed
-lemma wf_lprod[recdef_wf,simp,intro]:
+lemma wf_lprod[simp,intro]:
assumes wf_R: "wf R"
shows "wf (lprod R)"
proof -
@@ -116,7 +116,7 @@
by (auto intro: lprod_list[where a=c and b=c and
ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
-lemma [recdef_wf, simp, intro]:
+lemma [simp, intro]:
assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
proof -
have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
@@ -125,7 +125,7 @@
by (rule_tac wf_subset, auto)
qed
-lemma [recdef_wf, simp, intro]:
+lemma [simp, intro]:
assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
proof -
have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
--- a/src/HOL/ZF/Zet.thy Mon Aug 01 20:21:11 2011 +0200
+++ b/src/HOL/ZF/Zet.thy Tue Aug 02 10:03:12 2011 +0200
@@ -196,7 +196,7 @@
lemma zimage_id[simp]: "zimage id A = A"
by (simp add: zet_ext_eq zimage_iff)
-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"
+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"
by (auto simp add: zet_ext_eq zimage_iff)
end