src/HOL/Hilbert_Choice.thy
changeset 57213 9daec42f6784
parent 56740 5ebaa364d8ab
child 57275 0ddb5b755cdc
equal deleted inserted replaced
57212:f25dad3d6144 57213:9daec42f6784