# HG changeset patch
# User berghofe
# Date 1247584657 -7200
# Node ID 400a519bc888b54132bd9477590675ea7e24a0b0
# Parent  4127b89f48abfc6014996857f94c237e62de6b57
Use term antiquotation to refer to constant names in subsection title.

diff -r 4127b89f48ab -r 400a519bc888 src/HOL/Fact.thy
--- 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