# HG changeset patch
# User haftmann
# Date 1240769870 -7200
# Node ID 081e825c22186e63e9b947d4d68d0ebb28c148aa
# Parent  648d02b124d8db9d68a22bb21e8a6da6dab0863f
fixed document generation

diff -r 648d02b124d8 -r 081e825c2218 src/HOL/Power.thy
--- 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)