src/HOL/Hilbert_Choice.thy
changeset 12329 8743e8305611
parent 12298 b344486c33e2
child 12372 cd3a09c7dac9