# HG changeset patch
# User huffman
# Date 1231779865 28800
# Node ID 0139c9a01ca44c1b88fb410f0ec59c668800791e
# Parent  b0f586f38dd7c56095603885ce6a0a799a2b341b
add list-style syntax for pCons

diff -r b0f586f38dd7 -r 0139c9a01ca4 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Mon Jan 12 08:46:07 2009 -0800
+++ b/src/HOL/Polynomial.thy	Mon Jan 12 09:04:25 2009 -0800
@@ -100,6 +100,13 @@
 where
   [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"
 
+syntax
+  "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
+
+translations
+  "[:x, xs:]" == "CONST pCons x [:xs:]"
+  "[:x:]" == "CONST pCons x 0"
+
 lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
   unfolding Poly_def by (auto split: nat.split)