src/HOL/Hilbert_Choice.thy
changeset 22505 e2d378a97905
parent 21999 0cf192e489e2
child 22690 0b08f218f260