src/HOL/Algebra/FiniteProduct.thy

       then foldD (carrier G) (mult G o f) \<one> A
       else arbitrary"
 
 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
 syntax (xsymbols)
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 syntax (HTML output)
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
 
 ML_setup {* 
   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;