src/HOL/Hilbert_Choice.thy
changeset 58187 d2ddd401d74d
parent 58092 4ae52c60603a
child 58481 62bc7c79212b