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.
dropped stupid name
authorkrauss
Mon, 21 Feb 2011 23:14:36 +0100
changeset 41810 588c95c4b53e
parent 41809 6799f95479e2
child 41811 7e338ccabff0
dropped stupid name
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy file | annotate | diff | comparison | revisions 
--- 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') ;
isabelle