src/HOL/Library/OptionalSugar.thy
changeset 61536 346aa2c5447f
parent 61143 5f898411ce87
child 61645 ae5e55d03e45