src/HOL/Option.thy
changeset 8959 9d793220a46a
parent 5445 3905974ad555
child 9001 93af64f54bf2
equal deleted inserted replaced
8958:ba75f564726b 8959:9d793220a46a