--- a/src/HOL/Nat_Numeral.thy Mon Feb 08 14:22:22 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Mon Feb 08 14:22:22 2010 +0100 @@ -113,7 +113,7 @@ end -context linlinordered_ring_strict +context linordered_ring_strict begin lemma sum_squares_ge_zero: