src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 61586 5197a2ecb658
parent 61166 5976fe402824
child 62390 842917225d56
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 05 10:39:49 2015 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Nov 05 10:39:59 2015 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4  | "polysize (Pw p n) = 1 + polysize p"
     1.5  | "polysize (CN c n p) = 4 + polysize c + polysize p"
     1.6  
     1.7 -primrec polybound0:: "poly \<Rightarrow> bool" -- \<open>a poly is INDEPENDENT of Bound 0\<close>
     1.8 +primrec polybound0:: "poly \<Rightarrow> bool" \<comment> \<open>a poly is INDEPENDENT of Bound 0\<close>
     1.9  where
    1.10    "polybound0 (C c) \<longleftrightarrow> True"
    1.11  | "polybound0 (Bound n) \<longleftrightarrow> n > 0"
    1.12 @@ -41,7 +41,7 @@
    1.13  | "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p"
    1.14  | "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p"
    1.15  
    1.16 -primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" -- \<open>substitute a poly into a poly for Bound 0\<close>
    1.17 +primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" \<comment> \<open>substitute a poly into a poly for Bound 0\<close>
    1.18  where
    1.19    "polysubst0 t (C c) = C c"
    1.20  | "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)"