--- a/NEWS Fri Nov 28 10:52:32 1997 +0100
+++ b/NEWS Fri Nov 28 10:54:13 1997 +0100
@@ -89,6 +89,10 @@
* added prems argument to simplification procedures;
+* HOL, FOL, ZF: added infix function `addsplits':
+ instead of `<simpset> setloop (split_tac <thms>)'
+ you can simply write `<simpset> addsplits <thms>'
+
*** Syntax ***
@@ -113,16 +117,12 @@
* HOL/Map: new theory of `maps' a la VDM;
-* HOL/simplifier: added infix function `addsplits':
- instead of `<simpset> setloop (split_tac <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)
+ `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
are rewritten to
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
and those of the form
- `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
+ `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)' (or t=x)
are rewritten to
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',