src/HOL/Predicate.thy
changeset 23853 2c69bb1374b8
parent 23741 1801a921df13
child 24345 86a3557a9ebb