src/HOL/Algebra/Congruence.thy
changeset 28381 0b8237df37bd
parent 27717 21bbd410ba04
child 29237 e90d9d51106b