src/HOL/Hilbert_Choice.thy
changeset 45300 d8c8c2fcab2c
parent 44921 58eef4843641
child 45607 16b4f5774621