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
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
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
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 relevant to
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
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: In
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 as
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
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
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
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 Sun, 7 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius makar...@sketis.net:
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
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 Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
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
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
15 matches
Mail list logo
