src/HOL/Option.ML
changeset 4578 9f79e84ce00d
parent 4477 b3e5857d8d99
child 4752 1c334bd00038
equal deleted inserted replaced
4577:674b0b354feb 4578:9f79e84ce00d