Skip to content
Success

Changes

Summary

  1. merged
  2. Map.map_of movement
  3. removed Map from docu
  4. move map_of to List
Changeset 77268:9653bea4aa83 by nipkow:
merged
Changeset 77267:1fde0e4fd791 by nipkow:
Map.map_of movement
The file was modified NEWS (diff)
Changeset 77266:334015f9098e by nipkow:
removed Map from docu
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/HOL/Data_Structures/Trie_Map.thy (diff)
Changeset 77265:bafdc56654cf by nipkow:
move map_of to List
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Map.thy (diff)