src/HOL/Hilbert_Choice.thy
changeset 18052 004515accc10
parent 17893 aef5a6d11c2a
child 18389 8352b1d3b639