--- 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])"