src/HOL/Old_Number_Theory/Chinese.thy

-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/Chinese.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* The Chinese Remainder Theorem *}
 

 *}
 
 
 subsection {* Definitions *}
 
-consts
-  funprod :: "(nat => int) => nat => nat => int"
-  funsum :: "(nat => int) => nat => nat => int"
-
-primrec
+primrec funprod :: "(nat => int) => nat => nat => int"
+where
   "funprod f i 0 = f i"
-  "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
-
-primrec
+| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
+
+primrec funsum :: "(nat => int) => nat => nat => int"
+where
   "funsum f i 0 = f i"
-  "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
+| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
 
 definition
   m_cond :: "nat => (nat => int) => bool" where
   "m_cond n mf =
     ((\<forall>i. i \<le> n --> 0 < mf i) \<and>