src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41810 588c95c4b53e
parent 41808 9f436d00248f
child 41811 7e338ccabff0
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Feb 21 23:14:36 2011 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4    "polyadd (C c, C c') = C (c+\<^sub>Nc')"
     1.5    "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
     1.6    "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
     1.7 -stupid:  "polyadd (CN c n p, CN c' n' p') = 
     1.8 +  "polyadd (CN c n p, CN c' n' p') =
     1.9      (if n < n' then CN (polyadd(c,CN c' n' p')) n p
    1.10       else if n'<n then CN (polyadd(CN c n p, c')) n' p'
    1.11       else (let cc' = polyadd (c,c') ;