--- a/src/HOL/Fact.thy Thu Oct 29 11:41:36 2009 +0100
+++ b/src/HOL/Fact.thy Thu Oct 29 11:41:37 2009 +0100
@@ -8,7 +8,7 @@
header{*Factorial Function*}
theory Fact
-imports Nat_Transfer
+imports Main
begin
class fact =
@@ -266,9 +266,6 @@
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
by auto
-class ordered_semiring_1 = ordered_semiring + semiring_1
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
-
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"