src/HOL/Hilbert_Choice.thy
changeset 17780 274eaa114c6d
parent 17702 ea88ddeafabe
child 17893 aef5a6d11c2a
equal deleted inserted replaced
17779:407bea05c2da 17780:274eaa114c6d