Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
redundant;
authorwenzelm
Wed, 16 Oct 2024 20:22:20 +0200
changeset 81175 20b4fc5914e6
parent 81174 3c262e273ebd
child 81176 c0522b2d3df6
redundant;
src/HOL/Computational_Algebra/Polynomial.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle