1.1 --- a/src/HOL/Fact.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Fact.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -266,15 +266,15 @@
     1.4  lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
     1.5  by auto
     1.6  
     1.7 -lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
     1.8 +lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
     1.9  
    1.10 -lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
    1.11 +lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
    1.12  by simp
    1.13  
    1.14 -lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::ordered_field) < inverse (of_nat (fact n))"
    1.15 +lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
    1.16  by (auto simp add: positive_imp_inverse_positive)
    1.17  
    1.18 -lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::ordered_field) \<le> inverse (of_nat (fact n))"
    1.19 +lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
    1.20  by (auto intro: order_less_imp_le)
    1.21  
    1.22  end