src/HOL/Hilbert_Choice.thy
changeset 21404 eb85850d3eb7
parent 21243 afffe1f72143
child 21999 0cf192e489e2