src/HOL/Hilbert_Choice.thy
changeset 16600 55ffcee3b8f3
parent 16563 a92f96951355
child 16796 140f1e0ea846