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)"
```