--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Mon Apr 25 16:09:26 2016 +0200
@@ -133,7 +133,7 @@
fix x
assume "x \<in> f y' ` Y"
then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
- def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
+ define y'' where "y'' = (if y \<sqsubseteq> y' then y' else y)"
from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])