src/HOL/Hilbert_Choice.thy
changeset 65045 b69ef432438d
parent 64591 240a39af9ec4
child 65815 416aa3b00cbe