src/HOL/Option.thy
changeset 80137 0c51e0a6bc37
parent 69275 9bbd5497befd