| changeset 33524 | a08e6c1cbc04 |
| parent 33472 | e88f67d679c4 |
| child 33627 | ffb4a811e34d |
--- a/NEWS Sun Nov 08 19:15:37 2009 +0100 +++ b/NEWS Sun Nov 08 21:00:05 2009 +0100 @@ -236,6 +236,11 @@ *** ML *** +* Theory and context data is now introduced by the simplified and +modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs +to be pure, but the old TheoryDataFun for mutable data (with explicit +copy operation) is still available for some time. + * Removed some old-style infix operations using polymorphic equality. INCOMPATIBILITY.