src/HOL/Library/Complete_Partial_Order2.thy
changeset 63040 eb4ddd18d635
parent 62858 d72a6f9ee690
child 63092 a949b2a5f51d
--- 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])