src/HOL/Map.ML
changeset 5071 548f398d770b
parent 5069 3ea049f7979d
child 5143 b94cd208f073