src/HOL/ex/RPred.thy
changeset 51618 a3577cd80c41
parent 44845 5e51075cbd97