src/HOL/Hilbert_Choice.thy
changeset 64722 6df73de0d3c7
parent 64591 240a39af9ec4
child 65815 416aa3b00cbe