src/HOL/Hilbert_Choice.thy
changeset 63572 c0cbfd2b5a45
parent 63540 f8652d0534fa
child 63612 7195acc2fe93