src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 53374 a14d2a854c02
parent 52803 bcaa5bbf7e6b
child 54220 0e6645622f22
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -1314,7 +1314,7 @@
     1.4          head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
     1.5        have ?case by simp}
     1.6      moreover
     1.7 -    {moreover assume nz: "n = 0"
     1.8 +    { assume nz: "n = 0"
     1.9        from polymul_degreen[OF norm(5,4), where m="0"]
    1.10          polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
    1.11        norm(5,6) degree_npolyhCN[OF norm(6)]