src/HOL/Algebra/Congruence.thy
changeset 28052 4dc09699cf93
parent 27717 21bbd410ba04
child 29237 e90d9d51106b