src/HOL/Hilbert_Choice.thy
changeset 21258 62f25a96f0c1
parent 21243 afffe1f72143
child 21999 0cf192e489e2