# HG changeset patch
# User nipkow
# Date 1677186272 -3600
# Node ID 1f5428d66591beb3e7b0a7269b93515ef14d0088
# Parent  b23367be605163621aab5625f38253aeabd9486f
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation

diff -r b23367be6051 -r 1f5428d66591 NEWS
--- a/NEWS	Thu Feb 23 15:37:17 2023 +0100
+++ b/NEWS	Thu Feb 23 22:04:32 2023 +0100
@@ -51,6 +51,9 @@
   - Renamed lemma inj_on_strict_subset to image_strict_mono.
     Minor INCOMPATIBILITY.
 
+* Theory HOL.Map:
+  - Map.empty has been demoted to an input abbreviation only
+
 * Theory "HOL.Relation":
   - Added predicates irrefl_on and irreflp_on and redefined irrefl and
     irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
diff -r b23367be6051 -r 1f5428d66591 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Feb 23 15:37:17 2023 +0100
+++ b/src/HOL/Map.thy	Thu Feb 23 22:04:32 2023 +0100
@@ -14,7 +14,7 @@
 
 type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
 
-abbreviation
+abbreviation (input)
   empty :: "'a \<rightharpoonup> 'b" where
   "empty \<equiv> \<lambda>x. None"