src/HOL/ex/RPred.thy
changeset 47817 5d2d63f4363e
parent 44845 5e51075cbd97