src/HOL/Groups_List.thy
changeset 61799 4cf66f21b764
parent 61776 57bb7da5c867
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Groups_List.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Groups_List.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  syntax (xsymbols)
     1.5    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
     1.6  
     1.7 -translations -- \<open>Beware of argument permutation!\<close>
     1.8 +translations \<comment> \<open>Beware of argument permutation!\<close>
     1.9    "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    1.10    "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    1.11  
    1.12 @@ -179,7 +179,7 @@
    1.13    "(\<Sum>x\<leftarrow>xs. 0) = 0"
    1.14    by (induct xs) (simp_all add: distrib_right)
    1.15  
    1.16 -text\<open>For non-Abelian groups @{text xs} needs to be reversed on one side:\<close>
    1.17 +text\<open>For non-Abelian groups \<open>xs\<close> needs to be reversed on one side:\<close>
    1.18  lemma (in ab_group_add) uminus_listsum_map:
    1.19    "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
    1.20    by (induct xs) simp_all
    1.21 @@ -357,7 +357,7 @@
    1.22  syntax (xsymbols)
    1.23    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.24  
    1.25 -translations -- \<open>Beware of argument permutation!\<close>
    1.26 +translations \<comment> \<open>Beware of argument permutation!\<close>
    1.27    "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    1.28    "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    1.29