src/HOL/Hilbert_Choice.thy
changeset 63908 ca41b6670904
parent 63807 5f77017055a3
child 63980 f8e556c8ad6f
equal deleted inserted replaced
63907:36bac3d245d9 63908:ca41b6670904