src/HOL/Option.thy
changeset 78851 db37cae970a6
parent 69275 9bbd5497befd
child 81706 7beb0cf38292