src/HOL/Library/OptionalSugar.thy
changeset 81954 6f2bcdfa9a19
parent 81136 2b949a3bfaac