# HG changeset patch # User wenzelm # Date 1452278790 -3600 # Node ID 686681f69d5e5ce89e785fa9789d143aad9ae3e6 # Parent fb73c0d7bb37e642e084f0f88fe11646fadef2f5 tuned; diff -r fb73c0d7bb37 -r 686681f69d5e src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Fri Jan 08 18:18:40 2016 +0100 +++ b/src/HOL/Algebra/FiniteProduct.thy Fri Jan 08 19:46:30 2016 +0100 @@ -298,7 +298,7 @@ "_finprod" :: "index => idt => 'a set => 'b => 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations - "\\i\A. b" \ "CONST finprod \\ (%i. b) A" + "\\<^bsub>G\<^esub>i\A. b" \ "CONST finprod G (%i. b) A" -- \Beware of argument permutation!\ lemma (in comm_monoid) finprod_empty [simp]: diff -r fb73c0d7bb37 -r 686681f69d5e src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Fri Jan 08 18:18:40 2016 +0100 +++ b/src/HOL/Algebra/Ring.thy Fri Jan 08 19:46:30 2016 +0100 @@ -38,7 +38,7 @@ "_finsum" :: "index => idt => 'a set => 'b => 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations - "\\i\A. b" \ "CONST finsum \\ (%i. b) A" + "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (%i. b) A" -- \Beware of argument permutation!\