src/HOL/Predicate.thy
changeset 43333 2bdec7f430d3
parent 41550 efa734d9b221
child 44007 b5e7594061ce