changeset 81091 | c007e6d9941d |
parent 81090 | 843dba3d307a |
child 81175 | 20b4fc5914e6 |
--- a/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 23:32:26 2024 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Oct 01 20:39:16 2024 +0200 @@ -350,8 +350,6 @@ syntax "_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>) -syntax_consts - pCons translations "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]" "[:x:]" \<rightleftharpoons> "CONST pCons x 0"