src/HOL/Hilbert_Choice.thy
changeset 62611 dc7cc407c911
parent 62521 6383440f41a8
child 62683 ddd1c864408b