NEWS
changeset 3930 84ef550f5066
parent 3901 8b09bc500f65
child 3943 b6e0c90f3bf4
     1.1 --- a/NEWS	Fri Oct 17 19:07:56 1997 +0200
     1.2 +++ b/NEWS	Sat Oct 18 13:23:02 1997 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -75,6 +74,10 @@
     1.9  
    1.10  *** HOL ***
    1.11  
    1.12 +* HOL/simplifier: added infix function `addsplits':
    1.13 +  instead of `<simpset> setloop (split_tac <thms>)'
    1.14 +  you can simply write `<simpset> adsplits <thms>'
    1.15 +
    1.16  * HOL/simplifier: terms of the form
    1.17    `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
    1.18    are rewritten to