src/HOL/Hilbert_Choice.thy
changeset 17987 f8b45ab11400
parent 17893 aef5a6d11c2a
child 18389 8352b1d3b639