On Sat, 17 Aug 2013, Christian Sternagel wrote:
I propose to apply the following patch to the documentation of the function
package. (I found two tiny typos which could have been prevented by using
@{thm [source] ...} -- which might not have existed at the time of writing --
instead of @{text
Dear all,
I propose to apply the following patch to the documentation of the
function package. (I found two tiny typos which could have been
prevented by using @{thm [source] ...} -- which might not have existed
at the time of writing -- instead of @{text ...}, the patch (hopefully)
replaces
