changeset 77356 | 1f5428d66591 |
parent 77307 | f02c8a45c4c1 |
child 77361 | b34435f2a2bf |
--- 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"