[isabelle-dev] Highlighting of locale variables

Lars Noschinski noschinl at in.tum.de
Fri Apr 12 15:40:08 CEST 2013

On 12.04.2013 15:24, Makarius wrote:
> On Fri, 12 Apr 2013, Lars Noschinski wrote:
>> Rationale: In the locale context, these locale variables are morally
>> constants. Somebody suggested to highlight locale variables like
>> constants, but personally I'd prefer a highlighting similar to
>> variables obtained or fixed in a proof (maybe a non-bold orange?).
> Can you point to situations where this is still treated differently?
> Such incidents are mostly coming from the depths of time, as Larry
> usually calls this.

I was referring to variable fixed by a locale. In the example below, "F" 
is always rendered like a free variable (i.e. blue); although it's scope 
is not the lemma, but the locale.

locale dummy = fixes F :: 'a

lemma "P F"

> There are certain intermediate states, like undeclared frees that are
> implicitly fixed by the system infrastructure via "auto fix", but that
> is slightly different.

An oddity related to this is the let command. In the example below, "a" 
is rendered as an undeclared free. This feels wrong as writing such a 
statement seems perfectly fine, because constants and variables on the 
left hand side are generalized anyway.

notepad begin
   let "?X a" = "1 + a"

   -- Lars

More information about the isabelle-dev mailing list