src/HOL/Map.thy
changeset 5393 7299e531d481
parent 5300 2b1ca524ace8
child 7958 f531589c9fc1