src/HOL/Hilbert_Choice.thy
changeset 46844 5d9aab0c609c
parent 45607 16b4f5774621
child 46950 d0181abdbdac