src/HOL/Hilbert_Choice.thy
changeset 67730 f91c437f6f68
parent 67673 c8caefb20564
child 67829 2a6ef5ba4822
equal deleted inserted replaced
67729:5152afa6258f 67730:f91c437f6f68