# HG changeset patch
# User krauss
# Date 1298326476 -3600
# Node ID 6799f95479e2f5a4d6e28728db4bc1901f310378
# Parent  9f436d00248f20937290edf217b762a1e2c593d6
removed duplicate declarations

diff -r 9f436d00248f -r 6799f95479e2 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
@@ -2570,15 +2570,6 @@
   from qelim[OF th, of p bs] show ?thesis  unfolding frpar_def by auto
 qed
 
-declare polyadd.simps[code]
-lemma [simp,code]: "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') ; 
-               pp' = polyadd (p,p')
-           in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
-  by (simp add: Let_def stupid)
-
 
 section{* Second implemenation: Case splits not local *}