src/HOL/Algebra/Congruence.thy
changeset 29300 e841a9de5445
parent 29237 e90d9d51106b
child 35355 613e133966ea