equal
deleted
inserted
replaced
129 situations; |
129 situations; |
130 |
130 |
131 * Pure: generic 'sym' attribute which declares a rule both as pure |
131 * Pure: generic 'sym' attribute which declares a rule both as pure |
132 'elim?' and for the 'symmetric' operation; |
132 'elim?' and for the 'symmetric' operation; |
133 |
133 |
|
134 * Pure: marginal comments ``--'' may now occur just anywhere in the |
|
135 text; the fixed correlation with particular command syntax has been |
|
136 discontinued; |
|
137 |
134 * Pure/Provers/classical: simplified integration with pure rule |
138 * Pure/Provers/classical: simplified integration with pure rule |
135 attributes and methods; the classical "intro?/elim?/dest?" |
139 attributes and methods; the classical "intro?/elim?/dest?" |
136 declarations coincide with the pure ones; the "rule" method no longer |
140 declarations coincide with the pure ones; the "rule" method no longer |
137 includes classically swapped intros; "intro" and "elim" methods no |
141 includes classically swapped intros; "intro" and "elim" methods no |
138 longer pick rules from the context; also got rid of ML declarations |
142 longer pick rules from the context; also got rid of ML declarations |