# HG changeset patch
# User nipkow
# Date 1675943478 -3600
# Node ID e3e326a2dab52e1f65d1cca099d8450fe4c3219d
# Parent  607e1e345e8f6dd139f8ad298c50a05177d65b86
tuned text

diff -r 607e1e345e8f -r e3e326a2dab5 src/HOL/Data_Structures/Map_Specs.thy
--- 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"