# HG changeset patch
# User haftmann
# Date 1265813532 -3600
# Node ID 4554bb2abfa3871cde6c6bac9278376d2619a3b2
# Parent  f36965a1fd420c08996d7b291d0f3df30abdc861
dropped last occurence of the linlinordered accident

diff -r f36965a1fd42 -r 4554bb2abfa3 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"