--- a/src/HOL/Groups_List.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Groups_List.thy Fri Oct 09 20:26:03 2015 +0200
@@ -107,8 +107,6 @@
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
@@ -376,8 +374,6 @@
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listprod" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
translations -- \<open>Beware of argument permutation!\<close>
"PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"