NEWS
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 ***