src/HOL/Hilbert_Choice.thy
changeset 71787 acfe72ff00c2
parent 71695 65489718f4dc
child 71827 5e315defb038