src/HOL/OperationalEquality.thy
changeset 20864 bb75b876b260
parent 20835 27d049062b56