src/HOL/Hilbert_Choice.thy
changeset 56805 8a87502c7da3
parent 56740 5ebaa364d8ab
child 57275 0ddb5b755cdc