src/HOL/Hilbert_Choice.thy
changeset 40535 732f0826f1ba
parent 39950 f3c4849868b8
child 40702 cf26dd7395e4