changeset 34259 | 2ba492b8b6e8 |
parent 34255 | 2dd2547acb41 |
child 34933 | 0652d00305be |
--- a/NEWS Mon Jan 04 22:43:07 2010 +0100 +++ b/NEWS Mon Jan 04 23:20:35 2010 +0100 @@ -47,6 +47,11 @@ * Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution. Rare INCOMPATIBILITY. +* Discontinued old TheoryDataFun with its copy/init operation -- data +needs to be pure. Functor Theory_Data_PP retains the traditional +Pretty.pp argument to merge, which is absent in the standard +Theory_Data version. + *** System ***