src/HOL/Algebra/Congruence.thy
changeset 69765 c5778547ed03
parent 68443 43055b016688
child 69895 6b03a8cf092d