src/HOL/Map.thy
changeset 5526 e7617b57a3e6
parent 5300 2b1ca524ace8
child 7958 f531589c9fc1