# HG changeset patch
# User krauss
# Date 1312272192 -7200
# Node ID f67c93f52d137c58ccaef6e27c4abec89c42523c
# Parent  823549d46960183377c5a3884c6bbe3c8a828902
eliminated obsolete recdef/wfrec related declarations

diff -r 823549d46960 -r f67c93f52d13 src/HOL/Bali/Basis.thy
--- 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]
diff -r 823549d46960 -r f67c93f52d13 src/HOL/ZF/Games.thy
--- 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)
diff -r 823549d46960 -r f67c93f52d13 src/HOL/ZF/LProd.thy
--- 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])"
diff -r 823549d46960 -r f67c93f52d13 src/HOL/ZF/Zet.thy
--- 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