src/HOL/Hilbert_Choice.thy
changeset 58176 710710a66173
parent 58092 4ae52c60603a
child 58481 62bc7c79212b