src/HOL/Predicate.thy
changeset 26984 d0e098e206f3
parent 26797 a6cb51c314f2
child 30328 ab47f43f7581