equal
deleted
inserted
replaced
71 |
71 |
72 |
72 |
73 *** General *** |
73 *** General *** |
74 |
74 |
75 * Meta-level proof terms (by Stefan Berghofer), see also ref manual; |
75 * Meta-level proof terms (by Stefan Berghofer), see also ref manual; |
|
76 |
|
77 * new token syntax "num" for plain numerals (without "#" of "xnum"); |
|
78 potential INCOMPATIBILITY, since -0, -1 etc. are now separate tokens, |
|
79 so expressions involving minus need to be spaced properly; |
76 |
80 |
77 * Classical reasoner: renamed addaltern to addafter, addSaltern to |
81 * Classical reasoner: renamed addaltern to addafter, addSaltern to |
78 addSafter; |
82 addSafter; |
79 |
83 |
80 * syntax: support non-oriented infixes; |
84 * syntax: support non-oriented infixes; |