diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Algebra/Ring.thy Thu May 26 17:51:22 2016 +0200 @@ -39,7 +39,7 @@ ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (%i. b) A" - -- \Beware of argument permutation!\ + \ \Beware of argument permutation!\ locale abelian_group = abelian_monoid + @@ -141,7 +141,7 @@ lemmas finsum_cong = add.finprod_cong text \Usually, if this rule causes a failed congruence proof error, - the reason is that the premise @{text "g \ B \ carrier G"} cannot be shown. + the reason is that the premise \g \ B \ carrier G\ cannot be shown. Adding @{thm [source] Pi_def} to the simpset is often useful.\ lemmas finsum_reindex = add.finprod_reindex @@ -206,7 +206,7 @@ lemmas (in abelian_group) minus_add = add.inv_mult -text \Derive an @{text "abelian_group"} from a @{text "comm_group"}\ +text \Derive an \abelian_group\ from a \comm_group\\ lemma comm_group_abelian_groupI: fixes G (structure) @@ -283,7 +283,7 @@ shows "cring R" proof (intro cring.intro ring.intro) show "ring_axioms R" - -- \Right-distributivity follows from left-distributivity and + \ \Right-distributivity follows from left-distributivity and commutativity.\ proof (rule ring_axioms.intro) fix x y z