src/HOL/Rings.thy
changeset 35097 4554bb2abfa3
parent 35092 cfe605c54e50
child 35216 7641e8d831d2
--- 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"