src/HOL/Algebra/RingHom.thy
changeset 81387 c677755779f5
parent 75963 884dbbc8e1b3
equal deleted inserted replaced
81386:bcd880130390 81387:c677755779f5