src/HOL/Option.thy
changeset 79720 deb3056ed823
parent 69275 9bbd5497befd
child 81706 7beb0cf38292
equal deleted inserted replaced
79719:8544f1045123 79720:deb3056ed823