| changeset 35845 | e5980f0ad025 |
| parent 35810 | a50237ec0ecd |
| child 35979 | 12bb31230550 |
--- a/NEWS Sat Mar 20 02:23:41 2010 +0100 +++ b/NEWS Sat Mar 20 17:33:11 2010 +0100 @@ -290,6 +290,10 @@ Pretty.pp argument to merge, which is absent in the standard Theory_Data version. +* Renamed varify/unvarify operations to varify_global/unvarify_global +to emphasize that these only work in a global situation (which is +quite rare). + *** System ***