src/HOL/Hilbert_Choice.thy
changeset 56812 baef1c110f12
parent 56740 5ebaa364d8ab
child 57275 0ddb5b755cdc