dropped last occurence of the linlinordered accident
authorhaftmann
Wed, 10 Feb 2010 15:52:12 +0100
changeset 35097 4554bb2abfa3
parent 35096 f36965a1fd42
child 35099 7722bcb5c37c
dropped last occurence of the linlinordered accident
src/HOL/Rings.thy
--- 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"