src/HOL/Predicate.thy
changeset 43871 79c3231e0593
parent 41550 efa734d9b221
child 44007 b5e7594061ce