--- 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]