author | paulson |
Thu, 09 Feb 2023 13:36:53 +0000 | |
changeset 77227 | 6c8c980e777a |
parent 77224 | e3e326a2dab5 (diff) |
parent 77226 | 69956724ad4f (current diff) |
child 77228 | 8c093a4b8ccf |
--- 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"