src/HOL/Hilbert_Choice.thy
changeset 81351 95cb584cb777
parent 80934 8e72f55295fd
child 81473 53e61087bc6f
equal deleted inserted replaced
81350:1818358373e2 81351:95cb584cb777