src/HOL/Library/OptionalSugar.thy
changeset 68658 16cc1161ad7f
parent 63935 aa1fe1103ab8