NEWS
changeset 17548 4949ab06913c
parent 17538 9b089c63f088
child 17564 0350ac95c4b6
equal deleted inserted replaced
17547:b0d70cf4ed18 17548:4949ab06913c
   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