# HG changeset patch
# User webertj
# Date 1180746935 -7200
# Node ID f96d909eda373dd1aeb876f46b269b44e3a8137b
# Parent  fabf2e8a7ba4689e6ff1d190268ccc44ee824936
cosmetic

diff -r fabf2e8a7ba4 -r f96d909eda37 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 02 00:09:02 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 02 03:15:35 2007 +0200
@@ -270,7 +270,7 @@
   in pick_vars discr (rineqs,replicate n Rat.zero) end;
 
 (* ------------------------------------------------------------------------- *)
-(* End of counter example finder. The actual decision procedure starts here. *)
+(* End of counterexample finder. The actual decision procedure starts here.  *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
@@ -548,7 +548,7 @@
   curry (op ~~) sds
   #> map print_atom
   #> commas
-  #> curry (op ^) "Counter example (possibly spurious):\n";
+  #> curry (op ^) "Counterexample (possibly spurious):\n";
 
 fun trace_ex (sg, params, atoms, discr, n, hist : history) =
   case hist of
@@ -563,7 +563,7 @@
           handle NoEx => NONE
     in
       case ex of
-        SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
+        SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
       | NONE => warning "arith failed"
     end;