src/HOL/Library/OptionalSugar.thy
changeset 22519 eb70ed79dac7
parent 21404 eb85850d3eb7
child 22835 37d3a984d730
equal deleted inserted replaced
22518:21c221e1c8eb 22519:eb70ed79dac7