src/HOL/Hilbert_Choice.thy
changeset 17601 a6a322f96145
parent 17420 bdcffa8d8665
child 17702 ea88ddeafabe