src/HOL/Hilbert_Choice.thy
changeset 21391 a8809f46bd7f
parent 21243 afffe1f72143
child 21999 0cf192e489e2