# HG changeset patch
# User wenzelm
# Date 1013542300 -3600
# Node ID b9635eb8a4489d1bb7b8866f46d819f667524095
# Parent  a70df1e5bf1023a8ca3cb9eadef13f0578a36aac
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;

diff -r a70df1e5bf10 -r b9635eb8a448 NEWS
--- a/NEWS	Tue Feb 12 20:28:27 2002 +0100
+++ b/NEWS	Tue Feb 12 20:31:40 2002 +0100
@@ -131,6 +131,10 @@
 * Pure: generic 'sym' attribute which declares a rule both as pure
 'elim?' and for the 'symmetric' operation;
 
+* Pure: marginal comments ``--'' may now occur just anywhere in the
+text; the fixed correlation with particular command syntax has been
+discontinued;
+
 * Pure/Provers/classical: simplified integration with pure rule
 attributes and methods; the classical "intro?/elim?/dest?"
 declarations coincide with the pure ones; the "rule" method no longer