src/HOL/Hilbert_Choice.thy
changeset 65143 36cd85caf09a
parent 64591 240a39af9ec4
child 65815 416aa3b00cbe