author | nipkow |
Thu, 09 Feb 2023 12:51:18 +0100 | |
changeset 77224 | e3e326a2dab5 |
parent 77223 | 607e1e345e8f |
child 77225 | b6f3eb537d91 |
child 77227 | 6c8c980e777a |
--- 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"