src/HOL/Hilbert_Choice.thy
changeset 63853 d0e8921da311
parent 63807 5f77017055a3
child 63980 f8e556c8ad6f