src/HOL/Predicate.thy
changeset 40920 977c60b622f4
parent 40813 f1fc2a1547eb
child 41075 4bed56dc95fb