1.1 --- a/src/HOL/Power.thy	Sun Apr 26 08:45:37 2009 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Apr 26 20:17:50 2009 +0200
     1.3 @@ -360,7 +360,7 @@
     1.4  context division_ring
     1.5  begin
     1.6  
     1.7 -text {* FIXME reorient or rename to nonzero_inverse_power *}
     1.8 +text {* FIXME reorient or rename to @{text nonzero_inverse_power} *}
     1.9  lemma nonzero_power_inverse:
    1.10    "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
    1.11    by (induct n)