src/HOL/Hilbert_Choice.thy
changeset 69912 dd55d2c926d9
parent 69861 62e47f06d22c
child 69913 ca515cf61651