src/HOL/Hilbert_Choice.thy
changeset 63412 def97df48390
parent 63374 1a474286f315
child 63540 f8652d0534fa