src/HOL/Hilbert_Choice.thy
changeset 65541 ae09b9f5980b
parent 64591 240a39af9ec4
child 65815 416aa3b00cbe