[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:
*** Inner syntax error⌂
Failed to parse term
Do I misunderstand this news entry? Or has this feature (silently)
This archive was generated by a fusion of
Pipermail (Mailman edition) and