src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Wed Jan 28 17:01:01 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Jan 29 16:51:17 2004 +0100
@@ -249,7 +249,8 @@
 apply (erule add_strict_left_mono)
 done
 
-lemma add_less_le_mono: "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
+lemma add_less_le_mono:
+     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
 apply (erule add_strict_right_mono [THEN order_less_le_trans])
 apply (erule add_left_mono) 
 done