src/HOL/Algebra/Congruence.thy
changeset 67907 02a14c1cb917
parent 67091 1393c2340eec
child 67999 1b05f74f2e5f