src/HOL/Hilbert_Choice.thy
changeset 59863 30519ff3dffb
parent 59094 9ced35b4a2a9
child 60585 48fdff264eb2
equal deleted inserted replaced
59862:44b3f4fa33ca 59863:30519ff3dffb