update map definition in Prog_Prove for new datatype package
authorkleing
Wed, 31 Dec 2014 11:27:26 +1100 (2014-12-31)
changeset 59204 0cbe0a56d3fa
parent 59203 5f0bd5afc16d
child 59205 663794ab87e6
update map definition in Prog_Prove for new datatype package
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