src/HOL/Power.thy
changeset 30997 081e825c2218
parent 30996 648d02b124d8
child 31001 7e6ffd8f51a9
--- 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)