# HG changeset patch
# User krauss
# Date 1298326476 -3600
# Node ID 588c95c4b53e7a9a5a60c683068ee94c6136831f
# Parent  6799f95479e2f5a4d6e28728db4bc1901f310378
dropped stupid name

diff -r 6799f95479e2 -r 588c95c4b53e src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
@@ -121,7 +121,7 @@
   "polyadd (C c, C c') = C (c+\<^sub>Nc')"
   "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
   "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
-stupid:  "polyadd (CN c n p, CN c' n' p') = 
+  "polyadd (CN c n p, CN c' n' p') =
     (if n < n' then CN (polyadd(c,CN c' n' p')) n p
      else if n'<n then CN (polyadd(CN c n p, c')) n' p'
      else (let cc' = polyadd (c,c') ;