src/HOL/OperationalEquality.thy
changeset 20618 3f763be47c2f
parent 20598 f8031b91c946
child 20835 27d049062b56