--- a/src/HOL/Wellfounded.thy Wed Jun 01 11:51:25 2011 +0200
+++ b/src/HOL/Wellfounded.thy Wed Jun 01 15:53:47 2011 +0200
@@ -864,7 +864,7 @@
lemma wf_bounded_measure:
fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
-assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
+assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
shows "wf r"
apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
apply (auto dest: assms)
@@ -873,11 +873,11 @@
lemma wf_bounded_set:
fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
assumes "!!a b. (b,a) : r \<Longrightarrow>
- finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
+ finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a"
shows "wf r"
apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
apply(drule assms)
-apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
+apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
done