src/HOL/Predicate.thy
changeset 44688 67b78d5dea5b
parent 44415 ce6cd1b2344b
child 44928 7ef6505bde7f