src/HOL/Option.thy
changeset 39214 49fc6c842d6c
parent 39159 0dec18004e75
child 39272 0b61951d2682
equal deleted inserted replaced
39213:297cd703f1f0 39214:49fc6c842d6c