src/HOL/Hilbert_Choice.thy
changeset 70178 4900351361b0
parent 70097 4005298550a6
child 70179 269dcea7426c