# HG changeset patch
# User nipkow
# Date 877173782 -7200
# Node ID 84ef550f50661a77bff41f067ebc2b3a3aff4070
# Parent  3553fcfa2c7e8bbc9b6d3bc8207bd1bf119daa61
addsplits

diff -r 3553fcfa2c7e -r 84ef550f5066 NEWS
--- a/NEWS	Fri Oct 17 19:07:56 1997 +0200
+++ b/NEWS	Sat Oct 18 13:23:02 1997 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
@@ -75,6 +74,10 @@
 
 *** HOL ***
 
+* HOL/simplifier: added infix function `addsplits':
+  instead of `<simpset> setloop (split_tac <thms>)'
+  you can simply write `<simpset> adsplits <thms>'
+
 * HOL/simplifier: terms of the form
   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
   are rewritten to