src/HOL/Hilbert_Choice.thy
changeset 40429 5f37c3964866
parent 39950 f3c4849868b8
child 40702 cf26dd7395e4