src/HOL/Tools/Presburger/cooper_proof.ML

 (*==================================================*)
 (*   Finding rho for modd_minusinfinity             *)
 (*==================================================*)
 fun rho_for_modd_minf x dlcm sg fm1 =
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
    val ctrue = cterm_of sg HOLogic.true_const
    val cfalse = cterm_of sg HOLogic.false_const
    val fm = norm_zero_one fm1
   in  case fm1 of 

 (* -------------------------------------------------------------*)
 (*                    Finding rho for pinf_modd                 *)
 (* -------------------------------------------------------------*)
 fun rho_for_modd_pinf x dlcm sg fm1 = 
 let
-    (*SOME certified Terms*)
+    (*Some certified Terms*)
     
   val ctrue = cterm_of sg HOLogic.true_const
   val cfalse = cterm_of sg HOLogic.false_const
   val fm = norm_zero_one fm1
  in  case fm1 of