src/HOL/Library/OptionalSugar.thy
changeset 30549 d2d7874648bd
parent 30503 201887dcea0a
child 30663 0b6aff7451b2