# HG changeset patch
# User paulson
# Date 908446514 -7200
# Node ID 38bda28c68a21022cb471bd2d529029e78cc1a8a
# Parent  1bac26652f4571b8df3a8bfe89b9f485f64bc411
integer simprocs

diff -r 1bac26652f45 -r 38bda28c68a2 NEWS
--- a/NEWS	Thu Oct 15 11:38:39 1998 +0200
+++ b/NEWS	Thu Oct 15 12:15:14 1998 +0200
@@ -193,6 +193,8 @@
 * reorganized the main HOL image: HOL/Integ and String loaded by
 default; theory Main includes everything;
 
+* automatic simplification of integer sums and comparisons, using cancellation;
+
 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
 
 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;