src/HOL/Algebra/RingHom.thy
changeset 70045 7b6add80e3a5
parent 70019 095dce9892e8
child 75963 884dbbc8e1b3
equal deleted inserted replaced
70044:da5857dbcbb9 70045:7b6add80e3a5