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 "(=" = "\\<^sub>f" begin subsection \Auxiliary constants and lemmas over @{type map}\