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
We probably still have a few occurrences of these, but no problem phasing them out. Cheers, Gerwin On 09.11.2018, at 10:03, Peter Lammich mailto:lamm...@in.tum.de>> wrote: I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ...

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

2018-11-08 Thread Peter Lammich
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 ofHowever, (* *) is still very important for informally andquickly commenting things out, also in inner

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