changeset 37591 | d3daea901123 |
parent 37536 | c62aa9281101 |
child 37608 | 165cd386288d |
--- a/NEWS Mon Jun 28 15:03:07 2010 +0200 +++ b/NEWS Mon Jun 28 15:03:07 2010 +0200 @@ -17,6 +17,10 @@ *** HOL *** +* Constant "split" has been merged with constant "prod_case"; names +of ML functions, facts etc. involving split have been retained so far, +though. INCOMPATIBILITY. + * Some previously unqualified names have been qualified: types