src/HOL/Library/Commutative_Ring.thy

   "Ipolex l (Neg P) = - Ipolex l P"
 
 text {* Create polynomial normalized polynomials given normalized inputs. *}
 
 definition
-  mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+  mkPinj :: "nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
   "mkPinj x P = (case P of
     Pc c \<Rightarrow> Pc c |
     Pinj y P \<Rightarrow> Pinj (x + y) P |
     PX p1 y p2 \<Rightarrow> Pinj x P)"
 
 definition
-  mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+  mkPX :: "'a::{comm_ring,recpower} pol \<Rightarrow> nat \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
   "mkPX P i Q = (case P of
     Pc c \<Rightarrow> (if (c = 0) then (mkPinj 1 Q) else (PX P i Q)) |
     Pinj j R \<Rightarrow> PX P i Q |
     PX P2 i2 Q2 \<Rightarrow> (if (Q2 = (Pc 0)) then (PX P2 (i+i2) Q) else (PX P i Q)) )"
 

   "neg (Pinj i P) = Pinj i (neg P)"
   "neg (PX P x Q) = PX (neg P) x (neg Q)"
 
 text {* Substraction *}
 definition
-  sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol"
+  sub :: "'a::{comm_ring,recpower} pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" where
   "sub p q = add (p, neg q)"
 
 text {* Square for Fast Exponentation *}
 primrec
   "sqr (Pc c) = Pc (c * c)"