[isabelle] String inner syntax



>From the NEWS file (Isabelle2014)

* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently, e.g. via cartouches).


Unfortunately, this seems not to work in Isabelle2018, and I cannot
find a NEWS entry that this had been discontinued.

e.g. in Isabelle 2018:

  term ‹''a''›
*** OK

  term ‹"a"›
*** Inner syntax error⌂
Failed to parse term


Do I misunderstand this news entry? Or has this feature (silently)
disappeared again?

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.