# HG changeset patch
# User wenzelm
# Date 1165275756 -3600
# Node ID fccafa917a680a941ccd9feff0c518d377137825
# Parent  c07b5b0e8492514701171fa7ea36e6aa119ef931
* Pure: official theorem names and additional comments are now strictly separate.

diff -r c07b5b0e8492 -r fccafa917a68 NEWS
--- a/NEWS	Tue Dec 05 00:30:38 2006 +0100
+++ b/NEWS	Tue Dec 05 00:42:36 2006 +0100
@@ -826,6 +826,11 @@
 allow natural usage in combination with the ||>, ||>>, |-> and
 fold_map combinators.
 
+* Pure: official theorem names (closed derivations) and additional
+comments (tags) are now strictly separate.  Name hints -- which are
+maintained as tags -- may be attached any time without affecting the
+derivation.
+
 * Pure: primitive rule lift_rule now takes goal cterm instead of an
 actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
 achieve the old behaviour.