src/HOL/Predicate.thy
changeset 33003 1c93cfa807bc
parent 32883 7cbd93dacef3
child 33104 560372b461e5