Summary
- merged
- Map.map_of movement
- removed Map from docu
- move map_of to List
The file was modified | NEWS (diff) |
The file was modified | src/Doc/Main/Main_Doc.thy (diff) |
The file was modified | src/HOL/Data_Structures/Trie_Map.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/Map.thy (diff) |