src/HOL/Hilbert_Choice.thy
changeset 25967 dd602eb20f3f
parent 23433 c2c10abd2a1e
child 26072 f65a7fa2da6c
equal deleted inserted replaced
25966:74f6817870f9 25967:dd602eb20f3f