src/HOL/Hilbert_Choice.thy
changeset 25322 e2eac0c30ff5
parent 23433 c2c10abd2a1e
child 26072 f65a7fa2da6c
equal deleted inserted replaced
25321:e34b2265698a 25322:e2eac0c30ff5