src/HOL/Num.thy
changeset 59867 58043346ca64
parent 59621 291934bac95e
child 59996 4dca48557921
     1.1 --- a/src/HOL/Num.thy	Tue Mar 31 16:49:41 2015 +0100
     1.2 +++ b/src/HOL/Num.thy	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -1075,7 +1075,7 @@
     1.4  
     1.5  subsection {* Particular lemmas concerning @{term 2} *}
     1.6  
     1.7 -context linordered_field_inverse_zero
     1.8 +context linordered_field
     1.9  begin
    1.10  
    1.11  lemma half_gt_zero_iff: