author | nipkow |
Tue, 21 Oct 1997 17:38:31 +0200 | |
changeset 3964 | f95d2fb6fac8 |
parent 3963 | 29c5ec9ecbaa |
child 3965 | 1d7b53e6a2cb |
--- a/NEWS Tue Oct 21 17:36:54 1997 +0200 +++ b/NEWS Tue Oct 21 17:38:31 1997 +0200 @@ -79,7 +79,7 @@ * HOL/simplifier: added infix function `addsplits': instead of `<simpset> setloop (split_tac <thms>)' - you can simply write `<simpset> adsplits <thms>' + you can simply write `<simpset> addsplits <thms>' * HOL/simplifier: terms of the form `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)