On Fri, 17 Aug 2012, Tobias Nipkow wrote:
Am 17/08/2012 21:51, schrieb Christian Urban:
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation.
Otherwise, we should all make reasonable effort
to
For the record:
I did not know that Tjark had conversed with Florian privately before.
This removes the main accusation on his
http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was
looking like he was seizing control of the draft started by Florian.
The email reads (in
On Sat, 18 Aug 2012, Florian Haftmann wrote:
For the record:
I did not know that Tjark had conversed with Florian privately before.
This removes the main accusation on his
http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was
looking like he was seizing control of the draft
On Fri, 17 Aug 2012, Tjark Weber wrote:
I had expected that ISABELLE_BUILD_OPTIONS would allow me to specify
default options for the isabelle build tool, for instance -v for
verbose output.
None of the regular tools ever had such a feature, for usedir it was
merely a historical accident.
Am 17/08/2012 15:15, schrieb Makarius:
I count this as trolling on this mailing list.
We all have our pet peeves.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Fri, 17 Aug 2012, Tobias Nipkow wrote:
Am 17/08/2012 15:15, schrieb Makarius:
I count this as trolling on this mailing list.
We all have our pet peeves.
Tjark can express that somewhere privately, not here on this mailing list.
Makarius
Tjark, you have no business here.
If you want to propose changes to the Isabelle repository, you can send
them the via email as hg changeset.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation.
Otherwise, we should all make reasonable effort
to welcome everybody on both, the isabelle-users
and isabelle-dev lists. After all, we like to
On Fri, 17 Aug 2012, Christian Urban wrote:
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation. Otherwise, we should
all make reasonable effort to welcome everybody on both, the
isabelle-users and
Am 17/08/2012 21:51, schrieb Christian Urban:
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation.
Otherwise, we should all make reasonable effort
to welcome everybody on both, the
When I've seen the complete_boolean_algebra incident on the other
thread my first impulse was to check how far the wiring of the class
package wrt. the Isabelle document markup was. In principle the prover
can provide useful clues in non-intrusive ways here, if done right.
E.g. in
(BTW, in
Scala ambiguity after additional imports is treated as an error, and
causes the conflicting name entries to be canceled out.)
I definitely like this!
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hello everyone,
Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle
would print a similar warning whenever a definition reuses a name that
is already in scope in the current context. For example, if a theory
defines a
Hello Isabelle developers.
I was recently reminded of one of the things on my wish-list for Isabelle: a
make -k mode in which the system continues for as long as possible and
reports as many errors as possible, rather than halting after the first one. I
think this would be generally useful to
On Tue, 7 Dec 2010, Thomas Sewell wrote:
I was recently reminded of one of the things on my wish-list for
Isabelle: a make -k mode in which the system continues for as long as
possible and reports as many errors as possible, rather than halting
after the first one. I think this would be
15 matches
Mail list logo
