src/HOL/OperationalEquality.thy
changeset 20872 528054ca23e3
parent 20835 27d049062b56