src/HOL/Induct/BinaryTree_Map.thy
changeset 14472 cba7c0a3ffb3
parent 14288 d149e3cbdb39
equal deleted inserted replaced
14471:5688b05b2575 14472:cba7c0a3ffb3