src/HOL/Library/Discrete.thy
changeset 63093 3081f7719df7
parent 62390 842917225d56
child 63516 76492eaf3dc1