src/HOL/Hilbert_Choice.thy
changeset 69242 c911716d29bb
parent 68975 5ce4d117cea7
child 69275 9bbd5497befd