src/HOL/Hilbert_Choice.thy
changeset 81273 d96c9cd44b60
parent 80934 8e72f55295fd
child 81473 53e61087bc6f