src/HOL/Hilbert_Choice.thy
changeset 39905 0bfaaa81fc62
parent 39900 549c00e0e89b
child 39943 0ef551d47783
equal deleted inserted replaced
39904:f9e89d36a31a 39905:0bfaaa81fc62