src/HOL/Hilbert_Choice.thy
changeset 13792 d1811693899c
parent 13764 3e180bf68496
child 14115 65ec3f73d00b
equal deleted inserted replaced
13791:3b6ff7ceaf27 13792:d1811693899c