src/HOL/Option.thy
changeset 3895 b2463861c86a
parent 2019 b45d9f2042e0
child 4133 0a08c2b9b1ed