src/HOL/Predicate.thy
changeset 26583 9f81ab1b7b64
parent 24345 86a3557a9ebb
child 26797 a6cb51c314f2