src/HOL/Hilbert_Choice.thy
changeset 33019 bcf56a64ce1a
parent 33014 85d7a096e63f
child 33057 764547b68538