src/HOL/Hilbert_Choice.thy
changeset 61578 6623c81cb15a
parent 61424 c3658c18b7bc
child 61799 4cf66f21b764