merged
authorpaulson
Thu, 09 Feb 2023 13:36:53 +0000
changeset 77227 6c8c980e777a
parent 77224 e3e326a2dab5 (diff)
parent 77226 69956724ad4f (current diff)
child 77228 8c093a4b8ccf
merged
--- a/src/HOL/Data_Structures/Map_Specs.thy	Thu Feb 09 13:36:25 2023 +0000
+++ b/src/HOL/Data_Structures/Map_Specs.thy	Thu Feb 09 13:36:53 2023 +0000
@@ -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"