author | haftmann |
Wed, 10 Feb 2010 15:52:12 +0100 | |
changeset 35097 | 4554bb2abfa3 |
parent 35096 | f36965a1fd42 |
child 35099 | 7722bcb5c37c |
src/HOL/Rings.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Rings.thy Wed Feb 10 15:14:06 2010 +0100 +++ b/src/HOL/Rings.thy Wed Feb 10 15:52:12 2010 +0100 @@ -686,7 +686,7 @@ end -class linlinordered_semiring_1_strict = linordered_semiring_strict + semiring_1 +class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 class mult_mono1 = times + zero + ord + assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"