src/HOL/ex/RPred.thy
changeset 51796 f0ee854aa2bd
parent 44845 5e51075cbd97