src/HOL/Fact.thy
changeset 33319 74f0dcc0b5fb
parent 32558 e6e1fc2e73cb
child 35028 108662d50512
     1.1 --- a/src/HOL/Fact.thy	Thu Oct 29 11:41:36 2009 +0100
     1.2 +++ b/src/HOL/Fact.thy	Thu Oct 29 11:41:37 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports Nat_Transfer
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  class fact =
    1.12 @@ -266,9 +266,6 @@
    1.13  lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
    1.14  by auto
    1.15  
    1.16 -class ordered_semiring_1 = ordered_semiring + semiring_1
    1.17 -class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
    1.18 -
    1.19  lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
    1.20  
    1.21  lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"