src/HOL/ex/RPred.thy
changeset 55400 1e8dd9cd320b
parent 44845 5e51075cbd97