src/HOL/Option.ML
changeset 3462 3472fa00b1d4
parent 3344 b3e39a2987c1
child 4032 4b1c69d8b767
equal deleted inserted replaced
3461:7bf1e7c40a0c 3462:3472fa00b1d4