* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
authorwenzelm
Tue Feb 12 20:31:40 2002 +0100 (2002-02-12)
changeset 12877b9635eb8a448
parent 12876 a70df1e5bf10
child 12878 2896f88180b9
* Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
NEWS
     1.1 --- a/NEWS	Tue Feb 12 20:28:27 2002 +0100
     1.2 +++ b/NEWS	Tue Feb 12 20:31:40 2002 +0100
     1.3 @@ -131,6 +131,10 @@
     1.4  * Pure: generic 'sym' attribute which declares a rule both as pure
     1.5  'elim?' and for the 'symmetric' operation;
     1.6  
     1.7 +* Pure: marginal comments ``--'' may now occur just anywhere in the
     1.8 +text; the fixed correlation with particular command syntax has been
     1.9 +discontinued;
    1.10 +
    1.11  * Pure/Provers/classical: simplified integration with pure rule
    1.12  attributes and methods; the classical "intro?/elim?/dest?"
    1.13  declarations coincide with the pure ones; the "rule" method no longer