src/HOL/Induct/BinaryTree_Map.thy
changeset 14472 cba7c0a3ffb3
parent 14288 d149e3cbdb39