fixed document generation
authorhaftmann
Sun Apr 26 20:17:50 2009 +0200 (2009-04-26)
changeset 30997081e825c2218
parent 30996 648d02b124d8
child 30998 b057748ccebe
fixed document generation
src/HOL/Power.thy
     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)