On Fri, 12 Apr 2013, Clemens Ballarin wrote:
foo (in l) ...
is equivalent to
context l
begin
foo ...
end
by construction. We cannot have just one of them.
That sounds a bit dogmatic. If additional commands are made available for
targets, then the syntax should clearly be more flexible
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
Quoting Florian Haftmann :
context B begin
context
begin
interpretation A
end
end
This looks attractive, but could you please elaborate the semantics:
- What would be the effect of the interpretation from the inner block on the
outer block?
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
The following may or may not be related: I recently spent some thought
on getting rid of the mandatory vs optional distinction of qualifiers.
In any case this will likely have considerable impact, so here's the
idea:
Currently there is the strange
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius :
On Tue, 26 Mar 2013, Florian Haftmann wrote:
Note that we have one more aspect in the back-end that could help here: the
'private' modifier.
What would the 'private' modifier do in general? This sounds like a new
concept.
I
OK. So, just to make sure that I get this right: for locales A and B
where A contains the theorem a
context B begin
context begin
interpretation x: A
end
theorems b = x.a
end
would enrich B by b but not x.a, right?
Clemens
Quoting Florian Haftmann :
context B begin
Hi Florian,
I do not object to your suggestion, and it is clearly in reach within
the current code base. But... it is a different thing. Your suggestion
is to make sublocale work in locale targets seamlessly. But something like
instantiation ...
begin
sublocale ...
instance ...
end
then
On Fri, 12 Apr 2013, Account Isatest wrote:
Test for platform at-poly-test failed. Log file attached.
[...]
Unfinished session(s): HOL-Predicate_Compile_Examples
Finished at Fri Apr 12 02:42:04 CEST 2013
0:46:56 elapsed time, 3:11:32 cpu time, factor 4.08
--- test FAILED --- Fri
On Fri, 12 Apr 2013, Lars Noschinski wrote:
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 prefe
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
On Fri, 12 Apr 2013, Lars Noschinski wrote:
I wonder whether it would be a good idea to distinguish the syntax
highlighting for free variables and free variables fixed by a locale
("locale variables"). It seems that this information is already
available to the IDE (these variables are marked a
Hi,
I wonder whether it would be a good idea to distinguish the syntax
highlighting for free variables and free variables fixed by a locale
("locale variables"). It seems that this information is already
available to the IDE (these variables are marked as "fixed" when hovering).
Rationale: I
On 04/12/2013 02:18 PM, Makarius wrote:
It looks like I need to discuss it further with Stefan Berghofer, because he
made some reforms there in 2005 that now seem to crash on us.
Hi Markus,
thanks for the example. Please note that I am on holiday the following two
weeks, so it'll
take some t
On Wed, 10 Apr 2013, Makarius wrote:
On Wed, 10 Apr 2013, Johannes Hölzl wrote:
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions which
call Envir.var_clash is not shown.
It is relatively easy to inst
Am 12/04/2013 13:59, schrieb Makarius:
> On Fri, 12 Apr 2013, Tobias Nipkow wrote:
>
>> Holger Gast has ben added to the Unix group isabelle, if that is what you
>> mean. He is a member of my chair for half a year, that is why, similar to all
>> other members of the chair.
>
> OK, so it is not re
On Fri, 12 Apr 2013, Tobias Nipkow wrote:
Holger Gast has ben added to the Unix group isabelle, if that is what
you mean. He is a member of my chair for half a year, that is why,
similar to all other members of the chair.
OK, so it is not relevant to Isabelle development at all?
We have this
Holger Gast has ben added to the Unix group isabelle, if that is what you mean.
He is a member of my chair for half a year, that is why, similar to all other
members of the chair.
Tobias
Am 12/04/2013 13:08, schrieb Makarius:
> This needs to be a broadcast, because there is no additional informat
This needs to be a broadcast, because there is no additional information
to guess from:
Some user "gasth" has been added as new super-user for Isabelle at TUM.
Who is working with him? What is his project?
Makarius
___
isabelle-dev mailing
17 matches
Mail list logo
