src/HOL/Hilbert_Choice.thy
changeset 21051 c49467a9c1e1
parent 21020 9af9ceb16d58
child 21243 afffe1f72143