src/HOL/Option.thy
changeset 9368 415587dff134
parent 9001 93af64f54bf2