author | haftmann |
Fri, 02 Jul 2010 10:47:50 +0200 | |
changeset 37681 | 6ec40bc934e1 |
parent 37680 | e893e45219c3 |
child 37682 | ad5489a6be48 |
child 37691 | 4915de09b4d3 |
child 37720 | 50a9e2fa4f6b |
--- a/NEWS Fri Jul 02 10:45:25 2010 +0200 +++ b/NEWS Fri Jul 02 10:47:50 2010 +0200 @@ -18,7 +18,7 @@ *** HOL *** * Abolished symbol type names: "prod" and "sum" replace "*" and "+" -respectively. INCOMPATBILITY. +respectively. INCOMPATIBILITY. * Constant "split" has been merged with constant "prod_case"; names of ML functions, facts etc. involving split have been retained so far,