src/HOL/Hilbert_Choice.thy
changeset 69022 e2858770997a
parent 68975 5ce4d117cea7
child 69275 9bbd5497befd