src/HOL/Hilbert_Choice.thy
changeset 31715 2eb55a82acd9
parent 31454 2c0959ab073f
child 31723 f5cafe803b55