--- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Apr 25 16:09:26 2016 +0200
@@ -590,7 +590,7 @@
S = {a..<b} \<or>
S = {a..b}"
proof -
- def lower \<equiv> "{x. \<exists>s\<in>S. s \<le> x}" and upper \<equiv> "{x. \<exists>s\<in>S. x \<le> s}"
+ define lower upper where "lower = {x. \<exists>s\<in>S. s \<le> x}" and "upper = {x. \<exists>s\<in>S. x \<le> s}"
with ivl have "S = lower \<inter> upper"
by auto
moreover