--- a/src/HOL/Algebra/RingHom.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Algebra/RingHom.thy Thu May 26 17:51:22 2016 +0200
@@ -8,7 +8,7 @@
section \<open>Homomorphisms of Non-Commutative Rings\<close>
-text \<open>Lifting existing lemmas in a @{text ring_hom_ring} locale\<close>
+text \<open>Lifting existing lemmas in a \<open>ring_hom_ring\<close> locale\<close>
locale ring_hom_ring = R?: ring R + S?: ring S
for R (structure) and S (structure) +
fixes h
@@ -102,7 +102,7 @@
subsection \<open>The Kernel of a Ring Homomorphism\<close>
---"the kernel of a ring homomorphism is an ideal"
+\<comment>"the kernel of a ring homomorphism is an ideal"
lemma (in ring_hom_ring) kernel_is_ideal:
shows "ideal (a_kernel R S h) R"
apply (rule idealI)