> 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 requi
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 th
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
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 update_cartouch
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 motivat
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 {* ... *
inner 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 parti
> 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-...@in
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
