src/HOL/Nat.thy
changeset 35028 108662d50512
parent 34208 a7acd6c68d9b
child 35047 1b2bae06c796
     1.1 --- a/src/HOL/Nat.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Nat.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -741,7 +741,7 @@
     1.4  done
     1.5  
     1.6  text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
     1.7 -instance nat :: ordered_semidom
     1.8 +instance nat :: linordered_semidom
     1.9  proof
    1.10    fix i j k :: nat
    1.11    show "0 < (1::nat)" by simp
    1.12 @@ -1289,7 +1289,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -context ordered_semidom
    1.17 +context linordered_semidom
    1.18  begin
    1.19  
    1.20  lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
    1.21 @@ -1316,7 +1316,7 @@
    1.22  lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
    1.23    by (simp add: not_less [symmetric] linorder_not_less [symmetric])
    1.24  
    1.25 -text{*Every @{text ordered_semidom} has characteristic zero.*}
    1.26 +text{*Every @{text linordered_semidom} has characteristic zero.*}
    1.27  
    1.28  subclass semiring_char_0
    1.29    proof qed (simp add: eq_iff order_eq_iff)
    1.30 @@ -1345,7 +1345,7 @@
    1.31  
    1.32  end
    1.33  
    1.34 -context ordered_idom
    1.35 +context linordered_idom
    1.36  begin
    1.37  
    1.38  lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"