src/HOL/Hilbert_Choice.thy
changeset 14360 e654599b114e
parent 14208 144f45277d5a
child 14399 dc677b35e54f