src/HOL/Option.ML
changeset 3339 cfa72a70f2b5
parent 3295 c9c99aa082fb
child 3344 b3e39a2987c1