src/HOL/Hilbert_Choice.thy
changeset 69242 c911716d29bb
parent 68975 5ce4d117cea7
child 69275 9bbd5497befd
equal deleted inserted replaced
69241:5426d266dcc5 69242:c911716d29bb