equal
deleted
inserted
replaced
348 |
348 |
349 subsection \<open>List-style syntax for polynomials\<close> |
349 subsection \<open>List-style syntax for polynomials\<close> |
350 |
350 |
351 syntax |
351 syntax |
352 "_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>) |
352 "_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>) |
|
353 syntax_consts |
|
354 "_poly" \<rightleftharpoons> pCons |
353 translations |
355 translations |
354 "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]" |
356 "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]" |
355 "[:x:]" \<rightleftharpoons> "CONST pCons x 0" |
357 "[:x:]" \<rightleftharpoons> "CONST pCons x 0" |
356 |
358 |
357 |
359 |