src/HOL/Option.thy
changeset 39214 49fc6c842d6c
parent 39159 0dec18004e75
child 39272 0b61951d2682