src/HOL/Predicate.thy
changeset 25779 ae71b21de8fb
parent 24345 86a3557a9ebb
child 26797 a6cb51c314f2