src/HOL/Hilbert_Choice.thy
changeset 21316 4d913b8bccf1
parent 21243 afffe1f72143
child 21999 0cf192e489e2