src/HOL/Hilbert_Choice.thy
changeset 58377 c6f93b8d2d8e
parent 58092 4ae52c60603a
child 58481 62bc7c79212b