src/HOL/Predicate.thy
changeset 24766 d0de4e48b526
parent 24345 86a3557a9ebb
child 26797 a6cb51c314f2