src/HOL/Hilbert_Choice.thy
changeset 54784 54f1ce13c140
parent 54744 1e7f2d296e19
child 55020 96b05fd2aee4