src/HOL/Option.thy
changeset 64377 c1db9e3fe0e2
parent 63648 f9f3006a5579
child 66364 fa3247e6ee4b