src/HOL/Option.ML
changeset 4223 f60e3d2c81d3
parent 4133 0a08c2b9b1ed
child 4477 b3e5857d8d99