src/HOL/Library/OptionalSugar.thy
changeset 55515 0e161deca64d
parent 55052 c602013f127e
child 56245 84fc7dfa3cd4