src/HOL/Hilbert_Choice.thy
changeset 18134 6450591da9f0
parent 17893 aef5a6d11c2a
child 18389 8352b1d3b639