Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use term antiquotation to refer to constant names in subsection title.
authorberghofe
Tue, 14 Jul 2009 17:17:37 +0200
changeset 32039 400a519bc888
parent 32038 4127b89f48ab
child 32040 830141c9e528
Use term antiquotation to refer to constant names in subsection title.
src/HOL/Fact.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle