src/HOL/Predicate.thy
changeset 24222 a8a28c15c5cc
parent 23741 1801a921df13
child 24345 86a3557a9ebb