So I went to the internet, and I found these:
https://isabelle.in.tum.de/library/HOL/HOL/Map.html (Map)
https://isabelle.in.tum.de/library/HOL/HOL-Library/Mapping.html (Mapping)
Two theories beginning with the word "Map". I read through them for a good while and I couldn't really discern any notable differences between them. Is there a time when I should use the former rather than the latter and vice versa?
Thanks in advance!
Map.thy gives you some vocabulary to talk about partial functions, written as 'a ⇀ 'b, which is an abbreviation for 'a ⇒ 'b option.
The Mapping theory, on the other hand, wraps that into a new type of partial functions, which is useful for code generation. If you tried to export code for things involving partial functions of type 'a ⇀ 'b, you would get literally 'a ⇒ 'b option in the exported code, which means that e.g. things like asking for the domain of such a function will simply not be executable.
With Mapping, on the other hand, you can export to a more sensible implementation of (finite) maps, such as association lists or red-black trees.
So, short answer: Don't worry about Mapping except if (and when) you want to export executable code.