diff -r 9f03b5f847cd -r 121289b1ae27 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jan 29 22:28:03 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jan 29 22:29:44 2009 +0100
@@ -1108,7 +1108,7 @@
 lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
 by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
 
-subsection{* Rule 3 is trivial and is given by fps_times_def*}
+subsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
 subsection{* Rule 5 --- summation and "division" by (1 - X)*}
 
 lemma fps_divide_X_minus1_setsum_lemma: