src/HOL/Option.thy
changeset 6330 e1faf0f6f2b8
parent 5445 3905974ad555
child 9001 93af64f54bf2