src/HOL/Hilbert_Choice.thy
changeset 46311 56fae81902ce
parent 45607 16b4f5774621
child 46950 d0181abdbdac
equal deleted inserted replaced
46310:8af202923906 46311:56fae81902ce