Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Gerwin.Klein
> On 09.11.2018, at 22:34, Makarius wrote: > > On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: >> We probably still have a few occurrences of these, but no problem >> phasing them out. > > In principle it is just a matter of applying "isabelle update_cartouches > -t", but it might

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 08/11/2018 21:32, Makarius wrote: > Over the decades we have accumulated funny quotation forms in Isabelle > syntax that are often hard to explain to new users (also to old users). I don't have a full overview of all the fine points yet, but the general idea is like this: * cartouches are

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: > We probably still have a few occurrences of these, but no problem > phasing them out. In principle it is just a matter of applying "isabelle update_cartouches -t", but it might require some coordination, especially on AFP. E.g. one could

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 09/11/2018 00:03, Peter Lammich wrote: > I sometimes see {* *} in old theory files, and find it funny to be > reminded that this was standard only 5 years ago ... from my side there > are no uses of this quotation remaining that I'd know of Indeed. Do you want to apply "isabelle

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 08/11/2018 21:36, Lawrence Paulson wrote: >> On 8 Nov 2018, at 20:32, Makarius wrote: >> >> In particular, what are the remaining uses of {* ... *}? > > I didn’t even know that existed. It was used a lot with the 'section' and 'text' commands until recently. That was actually its main

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Gerwin.Klein
rs ago ... from my side there are no uses of this quotation remaining that I'd know of However, (* *) is still very important for informally andquickly commenting things out, also in inner syntax! Peter Original Message Subject: [isabelle-dev] Remaining uses of {* ... *} quo

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Peter Lammich
syntax!Peter Original Message Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?From: Makarius To: isabelle-dev CC: Over the decades we have accumulated funny quotation forms in Isabellesyntax that are often hard to explain to new users (also to old users).In particular

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Lawrence Paulson
> On 8 Nov 2018, at 20:32, Makarius wrote: > > In particular, what are the remaining uses of {* ... *}? I didn’t even know that existed. But I use (*...*) to enclose arbitrary text or comment material out. ___ isabelle-dev mailing list

[isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Makarius
Over the decades we have accumulated funny quotation forms in Isabelle syntax that are often hard to explain to new users (also to old users). In particular, what are the remaining uses of {* ... *}? It should already be superseded by cartouches. There is also "isabelle update_cartouches" to get