src/HOL/Option.ML
changeset 4351 36b28f78ed1b
parent 4133 0a08c2b9b1ed
child 4477 b3e5857d8d99