src/HOL/Option.ML
changeset 4521 c7f56322a84b
parent 4477 b3e5857d8d99
child 4752 1c334bd00038