src/HOL/Library/OptionalSugar.thy
changeset 38826 f42f425edf24
parent 35250 92664dca6f20
child 38864 4abe644fcea5
equal deleted inserted replaced
38825:4ec3cbd95f25 38826:f42f425edf24