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