# HG changeset patch
# User kleing
# Date 1419985646 -39600
# Node ID 0cbe0a56d3fabef3d61f9b60b21feaa79e0973a2
# Parent  5f0bd5afc16d95c5c5532b7400329989221a801c
update map definition in Prog_Prove for new datatype package

diff -r 5f0bd5afc16d -r 0cbe0a56d3fa src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Tue Dec 30 23:45:03 2014 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Dec 31 11:27:26 2014 +1100
@@ -159,6 +159,9 @@
 declare [[names_short]]
 (*>*)
 datatype 'a list = Nil | Cons 'a "'a list"
+(*<*)
+for map: map
+(*>*)
 
 text{*
 \begin{itemize}
@@ -395,8 +398,8 @@
 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"}\\
-@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
-@{text"\""}@{thm list.map(2)}@{text"\""}
+@{text"\""}@{thm list.map(1) [of f]}@{text"\" |"}\\
+@{text"\""}@{thm list.map(2) [of f x xs]}@{text"\""}
 \end{isabelle}
 
 \ifsem