src/HOL/Predicate.thy
changeset 30434 9b94b1358b95
parent 30430 42ea5d85edcc
child 30948 7f699568a877
child 31105 95f66b234086