# HG changeset patch
# User wenzelm
# Date 1729102940 -7200
# Node ID 20b4fc5914e6c57113b73f99a513200a48fb4c99
# Parent  3c262e273ebdc758de48cfe8ac1a5b983a66522a
redundant;

diff -r 3c262e273ebd -r 20b4fc5914e6 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Oct 16 19:44:02 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Oct 16 20:22:20 2024 +0200
@@ -353,7 +353,6 @@
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
-  "[:x:]" \<leftharpoondown> "CONST pCons x (_constrain 0 t)"
 
 
 subsection \<open>Representation of polynomials by lists of coefficients\<close>