src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41809 6799f95479e2
parent 41413 64cd30d6b0b8
child 41816 7a55699805dc
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Feb 21 23:14:36 2011 +0100
     1.3 @@ -2570,15 +2570,6 @@
     1.4    from qelim[OF th, of p bs] show ?thesis  unfolding frpar_def by auto
     1.5  qed
     1.6  
     1.7 -declare polyadd.simps[code]
     1.8 -lemma [simp,code]: "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') ; 
    1.12 -               pp' = polyadd (p,p')
    1.13 -           in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
    1.14 -  by (simp add: Let_def stupid)
    1.15 -
    1.16  
    1.17  section{* Second implemenation: Case splits not local *}
    1.18