src/HOL/Hilbert_Choice.thy
changeset 39432 12d1be8ff862
parent 39302 d7728f65b353
child 39900 549c00e0e89b
equal deleted inserted replaced
39431:f5320aba6750 39432:12d1be8ff862