src/HOL/Integ/presburger.ML

   | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
   | add_term_typed_consts (_, cs) = cs;
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* SOME Types*)
+(* Some Types*)
 val bT = HOLogic.boolT;
 val bitT = HOLogic.bitT;
 val iT = HOLogic.intT;
 val binT = HOLogic.binT;
 val nT = HOLogic.natT;

     val sg = sign_of_thm st
     (* The Abstraction step *)
     val g' = if a then abstract_pres sg g else g
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
-    (* SOME simpsets for dealing with mod div abs and nat*)
+    (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss