--- a/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 20:30:59 2024 +0200
@@ -348,13 +348,10 @@
subsection \<open>List-style syntax for polynomials\<close>
-nonterminal poly_args
syntax
- "" :: "'a \<Rightarrow> poly_args" (\<open>_\<close>)
- "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args" (\<open>_,/ _\<close>)
- "_poly" :: "poly_args \<Rightarrow> 'a poly" (\<open>[:(_):]\<close>)
+ "_poly" :: "args \<Rightarrow> 'a poly" (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
syntax_consts
- "_poly_args" "_poly" \<rightleftharpoons> pCons
+ pCons
translations
"[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
"[:x:]" \<rightleftharpoons> "CONST pCons x 0"