src/HOL/Hilbert_Choice.thy
changeset 68449 6d0f1a5a16ea
parent 67951 655aa11359dc
child 68610 4fdc9f681479
equal deleted inserted replaced
68448:3d1517f3ba49 68449:6d0f1a5a16ea