| 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"