src/HOL/Library/OptionalSugar.thy
changeset 61657 5b878bc6ae98
parent 61143 5f898411ce87
child 61645 ae5e55d03e45