| changeset 32039 | 400a519bc888 |
| parent 32036 | 8a9228872fbd |
| child 32047 | c141f139ce26 |
--- a/src/HOL/Fact.thy Fri Jul 10 12:55:06 2009 -0400 +++ b/src/HOL/Fact.thy Tue Jul 14 17:17:37 2009 +0200 @@ -261,7 +261,7 @@ by (cases m) auto -subsection {* fact and of_nat *} +subsection {* @{term fact} and @{term of_nat} *} lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)" by auto