src/HOL/Predicate.thy
changeset 60451 1f2b29f78439
parent 60166 ff6c4ff5e7ab
child 60758 d8d85a8172b5