diff -r 255055554c67 -r 9ef583b08647 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -73,7 +73,7 @@
 
 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;
@@ -249,7 +249,7 @@
     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]