src/HOL/Predicate.thy
changeset 23767 7272a839ccd9
parent 23741 1801a921df13
child 24345 86a3557a9ebb