src/HOL/Hilbert_Choice.thy
changeset 68004 a8a20be7053a
parent 67951 655aa11359dc
child 68610 4fdc9f681479