src/HOL/Hilbert_Choice.thy
changeset 42065 2b98b4c2e2f1
parent 40703 d1fc454d6735
child 42284 326f57825e1a
equal deleted inserted replaced
42064:f4e53c8630c0 42065:2b98b4c2e2f1