dropped last occurence of the linlinordered accident
authorhaftmann
Wed Feb 10 15:52:12 2010 +0100 (2010-02-10)
changeset 350974554bb2abfa3
parent 35096 f36965a1fd42
child 35099 7722bcb5c37c
dropped last occurence of the linlinordered accident
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Wed Feb 10 15:14:06 2010 +0100
     1.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 15:52:12 2010 +0100
     1.3 @@ -686,7 +686,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class linlinordered_semiring_1_strict = linordered_semiring_strict + semiring_1
     1.8 +class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1
     1.9  
    1.10  class mult_mono1 = times + zero + ord +
    1.11    assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"