src/HOL/Hilbert_Choice.thy
changeset 21041 60e418260b4d
parent 21020 9af9ceb16d58
child 21243 afffe1f72143