Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned text
authornipkow
Thu, 09 Feb 2023 12:51:18 +0100
changeset 77224 e3e326a2dab5
parent 77223 607e1e345e8f
child 77225 b6f3eb537d91
child 77227 6c8c980e777a
tuned text
src/HOL/Data_Structures/Map_Specs.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Map_Specs.thy	Wed Feb 08 15:05:24 2023 +0000
+++ b/src/HOL/Data_Structures/Map_Specs.thy	Thu Feb 09 12:51:18 2023 +0100
@@ -6,7 +6,7 @@
 imports AList_Upd_Del
 begin
 
-text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close>
+text \<open>The basic map interface with @{typ "'a \<Rightarrow> 'b option"} based specification:\<close>
 
 locale Map =
 fixes empty :: "'m"
isabelle