equal
deleted
inserted
replaced
186 lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" |
186 lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" |
187 by simp |
187 by simp |
188 |
188 |
189 * Inner syntax includes (*(*nested*) comments*). |
189 * Inner syntax includes (*(*nested*) comments*). |
190 |
190 |
191 * Pretty pinter now supports unbreakable blocks, specified in mixfix |
191 * Pretty printer now supports unbreakable blocks, specified in mixfix |
192 annotations as "(00...)". |
192 annotations as "(00...)". |
193 |
193 |
194 * Clear separation of logical types and nonterminals, where the latter |
194 * Clear separation of logical types and nonterminals, where the latter |
195 may only occur in 'syntax' specifications or type abbreviations. |
195 may only occur in 'syntax' specifications or type abbreviations. |
196 Before that distinction was only partially implemented via type class |
196 Before that distinction was only partially implemented via type class |