src/HOL/Hilbert_Choice.thy
changeset 42159 234ec7011e5d
parent 40703 d1fc454d6735
child 42284 326f57825e1a
equal deleted inserted replaced
42158:9bcecd429f77 42159:234ec7011e5d