Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Enclosed name containing _'s in @{text ...} antiquotation to make document
authorberghofe
Thu, 29 Jan 2009 22:29:44 +0100
changeset 29692 121289b1ae27
parent 29691 9f03b5f847cd
child 29693 708dcf7dec9f
Enclosed name containing _'s in @{text ...} antiquotation to make document preparation work again.
src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle