src/HOL/Option.ML
changeset 5184 9b8547a9496a
parent 5183 89f162de39cf
child 5293 4ce5539aa969
equal deleted inserted replaced
5183:89f162de39cf 5184:9b8547a9496a