src/HOL/Library/OptionalSugar.thy
changeset 22732 5bd1a2a94e1b
parent 21404 eb85850d3eb7
child 22835 37d3a984d730