src/HOL/Option.thy
changeset 2919 953a47dc0519
parent 2019 b45d9f2042e0
child 4133 0a08c2b9b1ed