src/HOL/Hilbert_Choice.thy
changeset 26113 ba5909699cc3
parent 26105 ae06618225ec
child 26347 105f55201077