| changeset 55108 | 0b7a0c1fdf7e |
| parent 55049 | 327eafb594ba |
| child 55114 | 0ee5c17f2207 |
--- a/NEWS Mon Jan 20 20:38:51 2014 +0100 +++ b/NEWS Wed Jan 22 15:10:33 2014 +0100 @@ -43,6 +43,10 @@ context discipline. See also Assumption.add_assumes and the more primitive Thm.assume_hyps. +* Inner syntax token language allows regular quoted strings "..." +(only makes sense in practice, if outer syntax is delimited +differently). + *** HOL ***