src/HOL/Hilbert_Choice.thy
changeset 24059 89a5382406a1
parent 23433 c2c10abd2a1e
child 26072 f65a7fa2da6c
equal deleted inserted replaced
24058:81aafd465662 24059:89a5382406a1