Re: [isabelle-dev] NEWS: discontinued old-style inner comments

2018-09-24 Thread Makarius
On 24/09/18 08:19, Lars Hupel wrote: >> There were a few remaining uses in AFP. Notable changes are >> AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources >> generated by LEM (!). I don't know how LEM is maintained: it needs to >> produce different inner comments next time, and can a

Re: [isabelle-dev] NEWS: discontinued old-style inner comments

2018-09-23 Thread Lars Hupel
> There were a few remaining uses in AFP. Notable changes are > AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources > generated by LEM (!). I don't know how LEM is maintained: it needs to > produce different inner comments next time, and can actually use > \ CARTOUCHE notation unifor

[isabelle-dev] NEWS: discontinued old-style inner comments

2018-09-23 Thread Makarius
*** General *** * Old-style inner comments (* ... *) within the term language are no longer supported (legacy feature in Isabelle2018). This refers to Isabelle/6e9df530b441. There were a few remaining uses in AFP. Notable changes are AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit so