src/HOL/Hilbert_Choice.thy
changeset 62540 f2fc5485e3b0
parent 62521 6383440f41a8
child 62683 ddd1c864408b