src/HOL/Hilbert_Choice.thy
changeset 74056 fb8d5c0133c9
parent 73623 5020054b3a16
child 74123 7c5842b06114