src/HOL/Hilbert_Choice.thy
changeset 21470 7c1b59ddcd56
parent 21243 afffe1f72143
child 21999 0cf192e489e2