src/HOL/Predicate.thy
changeset 26012 f6917792f8a4
parent 24345 86a3557a9ebb
child 26797 a6cb51c314f2