# HG changeset patch
# User wenzelm
# Date 1520445742 -3600
# Node ID 7655e6369c9f1d9a3be36f244910ee485d0a4364
# Parent  fd25580141966e4ec879f6f84046a2ada2be3913
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

diff -r fd2558014196 -r 7655e6369c9f src/HOL/Library/Finite_Map.thy
--- 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>
diff -r fd2558014196 -r 7655e6369c9f src/HOL/Map.thy
--- 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)