src/Doc/ProgProve/Bool_nat_list.thy
changeset 55465 0d31c0546286
parent 55320 8a6ee5c1f2e0
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Fri Feb 14 07:53:45 2014 +0100
@@ -394,8 +394,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 map.simps(1)}@{text"\" |"}\\
-@{text"\""}@{thm map.simps(2)}@{text"\""}
+@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
+@{text"\""}@{thm list.map(2)}@{text"\""}
 \end{isabelle}
 
 \ifsem