src/HOL/Hilbert_Choice.thy
changeset 16633 208ebc9311f2
parent 16563 a92f96951355
child 16796 140f1e0ea846
equal deleted inserted replaced
16632:ad2895beef79 16633:208ebc9311f2