src/HOL/Option.ML
changeset 4349 50403e5a44c0
parent 4133 0a08c2b9b1ed
child 4477 b3e5857d8d99