# HG changeset patch
# User nipkow
# Date 1421251459 -3600
# Node ID b1e5d552e8cc6bb3b4186a658253a0672c2529e9
# Parent  07b9893cd8a7cb126aa89995ec738fda87bfadf2
tuned

diff -r 07b9893cd8a7 -r b1e5d552e8cc src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Jan 14 15:22:50 2015 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Jan 14 17:04:19 2015 +0100
@@ -397,7 +397,7 @@
 @{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition),
 and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
 \begin{isabelle}
-\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
+\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \isacom{where}\\
 @{text"\""}@{thm list.map(1) [of f]}@{text"\" |"}\\
 @{text"\""}@{thm list.map(2) [of f x xs]}@{text"\""}
 \end{isabelle}