src/HOL/Library/OptionalSugar.thy
changeset 73182 a8a8bc42d552
parent 63935 aa1fe1103ab8
child 80914 d97fdabd9e2b
equal deleted inserted replaced
73181:02422c9add5e 73182:a8a8bc42d552