src/HOL/Hilbert_Choice.thy
changeset 17943 48ec47217fe2
parent 17893 aef5a6d11c2a
child 18389 8352b1d3b639