src/HOL/Option.ML
changeset 6330 e1faf0f6f2b8
parent 5520 e2484f1786b7
child 7030 53934985426a