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.
fixed document generation
authorhaftmann
Sun, 26 Apr 2009 20:17:50 +0200
changeset 30997 081e825c2218
parent 30996 648d02b124d8
child 30998 b057748ccebe
fixed document generation
src/HOL/Power.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Power.thy	Sun Apr 26 08:45:37 2009 +0200
+++ b/src/HOL/Power.thy	Sun Apr 26 20:17:50 2009 +0200
@@ -360,7 +360,7 @@
 context division_ring
 begin
 
-text {* FIXME reorient or rename to nonzero_inverse_power *}
+text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
 lemma nonzero_power_inverse:
   "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
   by (induct n)
isabelle