src/HOL/Hilbert_Choice.thy
changeset 61569 947ce60a06e1
parent 61424 c3658c18b7bc
child 61799 4cf66f21b764