src/HOL/Hilbert_Choice.thy
changeset 23357 16e0ec4bcd81
parent 22690 0b08f218f260
child 23433 c2c10abd2a1e