src/HOL/Predicate.thy
changeset 42148 d596e7bb251f
parent 41550 efa734d9b221
child 44007 b5e7594061ce