src/HOL/Algebra/Congruence.thy
changeset 71042 400e9512f1d3
parent 69895 6b03a8cf092d