--- a/src/HOL/Library/Extended.thy Mon Jun 01 18:59:20 2015 +0200
+++ b/src/HOL/Library/Extended.thy Mon Jun 01 18:59:20 2015 +0200
@@ -25,7 +25,7 @@
case_of_simps less_eq_extended_case: less_eq_extended.simps
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
-"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
+"((x::'a extended) < y) = (x \<le> y & \<not> y \<le> x)"
instance
by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)