# HG changeset patch
# User haftmann
# Date 1265635342 -3600
# Node ID 07dbdf60d5adb4966405b9bcc53dd7831cd69689
# Parent  a27b48967b266a1ef818afe08b315bec21ca519a
dropped accidental duplication of "lin" prefix from cs. 108662d50512

diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -637,7 +637,7 @@
   using eq_diff_eq[where a= x and b=t and c=0] by simp
 
 
-interpretation class_dense_linlinordered_field: constr_dense_linorder
+interpretation class_dense_linordered_field: constr_dense_linorder
  "op <=" "op <"
    "\<lambda> x y. 1/2 * ((x::'a::{linordered_field,number_ring}) + y)"
 proof (unfold_locales, dlo, dlo, auto)
@@ -871,7 +871,7 @@
    addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}]
 
 in
-Ferrante_Rackoff_Data.funs @{thm "class_dense_linlinordered_field.ferrack_axiom"}
+Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"}
   {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
 end
 *}
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -836,7 +836,7 @@
 lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
 lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
 lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_pos_le[simp]: "(0::'a\<Colon>linlinordered_ring_strict) <= x \<bullet> x"
+lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x"
   by (simp add: dot_def setsum_nonneg)
 
 lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
@@ -852,10 +852,10 @@
   show ?case by (simp add: h)
 qed
 
-lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
+lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
   by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)
 
-lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linlinordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
+lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
   by (auto simp add: le_less)
 
 subsection{* The collapse of the general concepts to dimension one. *}
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -501,12 +501,12 @@
 by transfer (rule power_mult_distrib)
 
 lemma hyperpow_two_le [simp]:
-  "(0::'a::{monoid_mult,linlinordered_ring_strict} star) \<le> r pow (1 + 1)"
+  "(0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow (1 + 1)"
 by (auto simp add: hyperpow_two zero_le_mult_iff)
 
 lemma hrabs_hyperpow_two [simp]:
   "abs(x pow (1 + 1)) =
-   (x::'a::{monoid_mult,linlinordered_ring_strict} star) pow (1 + 1)"
+   (x::'a::{monoid_mult,linordered_ring_strict} star) pow (1 + 1)"
 by (simp only: abs_of_nonneg hyperpow_two_le)
 
 lemma hyperpow_two_hrabs [simp]:
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -912,7 +912,7 @@
 
 instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
 
-instance star :: (linlinordered_semiring_strict) linlinordered_semiring_strict
+instance star :: (linordered_semiring_strict) linordered_semiring_strict
 apply (intro_classes)
 apply (transfer, erule (1) mult_strict_left_mono)
 apply (transfer, erule (1) mult_strict_right_mono)
@@ -936,7 +936,7 @@
 instance star :: (sgn_if) sgn_if
 by (intro_classes, transfer, rule sgn_if)
 
-instance star :: (linlinordered_ring_strict) linlinordered_ring_strict ..
+instance star :: (linordered_ring_strict) linordered_ring_strict ..
 instance star :: (ordered_comm_ring) ordered_comm_ring ..
 
 instance star :: (linordered_semidom) linordered_semidom
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -113,7 +113,7 @@
 
 end
 
-context linlinordered_ring_strict
+context linordered_ring_strict
 begin
 
 lemma sum_squares_ge_zero:
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Parity.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -218,7 +218,7 @@
   done
 
 lemma zero_le_even_power: "even n ==>
-    0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n"
+    0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
   apply (simp add: even_nat_equiv_def2)
   apply (erule exE)
   apply (erule ssubst)
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Ring_and_Field.thy	Mon Feb 08 14:22:22 2010 +0100
@@ -767,9 +767,9 @@
 
 end
 
-class linlinordered_semiring_1 = linordered_semiring + semiring_1
-
-class linlinordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
+class linordered_semiring_1 = linordered_semiring + semiring_1
+
+class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 begin
@@ -886,7 +886,7 @@
 
 end
 
-class linlinlinordered_semiring_1_strict = linlinordered_semiring_strict + semiring_1
+class linlinordered_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"
@@ -918,7 +918,7 @@
   assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
 begin
 
-subclass linlinordered_semiring_strict
+subclass linordered_semiring_strict
 proof
   fix a b c :: 'a
   assume "a < b" "0 < c"
@@ -1009,9 +1009,9 @@
 end
 
 (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
-   Basically, linordered_ring + no_zero_divisors = linlinordered_ring_strict.
+   Basically, linordered_ring + no_zero_divisors = linordered_ring_strict.
  *)
-class linlinordered_ring_strict = ring + linlinordered_semiring_strict
+class linordered_ring_strict = ring + linordered_semiring_strict
   + ordered_ab_group_add + abs_if
 begin
 
@@ -1207,7 +1207,7 @@
   (*previously linordered_ring*)
 begin
 
-subclass linlinordered_ring_strict ..
+subclass linordered_ring_strict ..
 subclass ordered_comm_ring ..
 subclass idom ..
 
@@ -1502,7 +1502,7 @@
   "(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric])
 
-lemma linlinordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
+lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
 proof
   fix x::'a
   have m1: "- (1::'a) < 0" by simp
@@ -1511,7 +1511,7 @@
   thus "\<exists>y. y < x" by blast
 qed
 
-lemma linlinordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
+lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
 proof
   fix x::'a
   have m1: " (1::'a) > 0" by simp
diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
@@ -581,11 +581,11 @@
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
      K EqCancelFactor.proc),
-    ("linlinordered_ring_le_cancel_factor",
+    ("linordered_ring_le_cancel_factor",
      ["(l::'a::linordered_ring) * m <= n",
       "(l::'a::linordered_ring) <= m * n"],
      K LeCancelFactor.proc),
-    ("linlinordered_ring_less_cancel_factor",
+    ("linordered_ring_less_cancel_factor",
      ["(l::'a::linordered_ring) * m < n",
       "(l::'a::linordered_ring) < m * n"],
      K LessCancelFactor.proc),