src/HOL/Hilbert_Choice.thy
changeset 60867 86e7560e07d0
parent 60758 d8d85a8172b5
child 60974 6a6f15d8fbc4
equal deleted inserted replaced
60866:7f562aa4eb4b 60867:86e7560e07d0