src/HOL/Library/OptionalSugar.thy
changeset 21619 dea0914773f7
parent 21404 eb85850d3eb7
child 22835 37d3a984d730