src/HOL/Hilbert_Choice.thy
changeset 56982 51d4189d95cf
parent 56740 5ebaa364d8ab
child 57275 0ddb5b755cdc
equal deleted inserted replaced
56981:3ef45ce002b5 56982:51d4189d95cf