src/HOL/Hilbert_Choice.thy
changeset 44350 63cddfbc5a09
parent 42284 326f57825e1a
child 44890 22f665a2e91c
equal deleted inserted replaced
44349:f057535311c5 44350:63cddfbc5a09