src/HOL/Library/OptionalSugar.thy
changeset 25595 6c48275f9c76
parent 22835 37d3a984d730
child 29494 a189c6274c7a
equal deleted inserted replaced
25594:43c718438f9f 25595:6c48275f9c76