src/HOL/Hilbert_Choice.thy
changeset 69148 d0517da45e5c
parent 68975 5ce4d117cea7
child 69275 9bbd5497befd
equal deleted inserted replaced
69147:6f4d561ea621 69148:d0517da45e5c