src/HOL/ex/RPred.thy
changeset 45940 71970a26a269
parent 44845 5e51075cbd97