src/HOL/Hilbert_Choice.thy
changeset 63908 ca41b6670904
parent 63807 5f77017055a3
child 63980 f8e556c8ad6f