src/HOL/Option.ML
changeset 8450 dc44d6533f0f
parent 8442 96023903c2df
child 9001 93af64f54bf2