--- a/src/HOL/Num.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Num.thy Tue Mar 31 21:54:32 2015 +0200
@@ -1075,7 +1075,7 @@
subsection {* Particular lemmas concerning @{term 2} *}
-context linordered_field_inverse_zero
+context linordered_field
begin
lemma half_gt_zero_iff: