> 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
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
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
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 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