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