src/HOL/Hilbert_Choice.thy
changeset 57362 3ae07451a9f5
parent 57275 0ddb5b755cdc
child 57448 159e45728ceb