| changeset 26660 | f978a6f48949 |
| parent 26659 | aae01f2139af |
| child 26681 | 19e1d3c96f2f |
--- a/NEWS Tue Apr 15 16:25:14 2008 +0200 +++ b/NEWS Tue Apr 15 18:49:12 2008 +0200 @@ -40,6 +40,8 @@ that tools may maintain dynamically scoped facts systematically, using PureThy.add_thms_dynamic. +* Command 'hide' now allows to hide from "fact" name space as well. + * Eliminated destructive theorem database, simpset, claset, and clasimpset. Potential INCOMPATIBILITY, really need to observe linear update of theories within ML code.