src/HOL/Algebra/Ring.thy
changeset 63167 0909deb8059b
parent 62105 686681f69d5e
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Algebra/Ring.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4        ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
     1.5  translations
     1.6    "\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (%i. b) A"
     1.7 -  -- \<open>Beware of argument permutation!\<close>
     1.8 +  \<comment> \<open>Beware of argument permutation!\<close>
     1.9  
    1.10  
    1.11  locale abelian_group = abelian_monoid +
    1.12 @@ -141,7 +141,7 @@
    1.13  
    1.14  lemmas finsum_cong = add.finprod_cong
    1.15  text \<open>Usually, if this rule causes a failed congruence proof error,
    1.16 -   the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
    1.17 +   the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
    1.18     Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
    1.19  
    1.20  lemmas finsum_reindex = add.finprod_reindex
    1.21 @@ -206,7 +206,7 @@
    1.22  
    1.23  lemmas (in abelian_group) minus_add = add.inv_mult
    1.24   
    1.25 -text \<open>Derive an @{text "abelian_group"} from a @{text "comm_group"}\<close>
    1.26 +text \<open>Derive an \<open>abelian_group\<close> from a \<open>comm_group\<close>\<close>
    1.27  
    1.28  lemma comm_group_abelian_groupI:
    1.29    fixes G (structure)
    1.30 @@ -283,7 +283,7 @@
    1.31    shows "cring R"
    1.32  proof (intro cring.intro ring.intro)
    1.33    show "ring_axioms R"
    1.34 -    -- \<open>Right-distributivity follows from left-distributivity and
    1.35 +    \<comment> \<open>Right-distributivity follows from left-distributivity and
    1.36            commutativity.\<close>
    1.37    proof (rule ring_axioms.intro)
    1.38      fix x y z