more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

--- a/src/HOL/Library/Finite_Map.thy	Wed Mar 07 17:39:18 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Wed Mar 07 19:02:22 2018 +0100
@@ -6,6 +6,7 @@
 
 theory Finite_Map
   imports FSet AList
+  abbrevs "(=" = "\<subseteq>\<^sub>f"
 begin
 
 subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>

--- a/src/HOL/Map.thy	Wed Mar 07 17:39:18 2018 +0100
+++ b/src/HOL/Map.thy	Wed Mar 07 19:02:22 2018 +0100
@@ -8,7 +8,8 @@
 section \<open>Maps\<close>
 
 theory Map
-imports List
+  imports List
+  abbrevs "(=" = "\<subseteq>\<^sub>m"
 begin
 
 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)