src/HOL/Algebra/Congruence.thy
changeset 61685 2b3772ecfdec
parent 61382 efac889fccbc
child 63167 0909deb8059b