src/HOL/Hilbert_Choice.thy
changeset 39994 7bd8013b903f
parent 39950 f3c4849868b8
child 40702 cf26dd7395e4