On 01/13/2012 06:24 PM, Makarius wrote:
I haven't been aware of that. The configuration goes back to myself, in
private communication with Alex. I did not check it later. In
4a892432e8f1 it is now more conventional, also tested manually to some
extend.
4a892432e8f1 merely modifies the setup for
Hi all,
> Here is what I suggest: If there is a concensus that the argument
> order of List.fold is more useful than the existing foldl, then we
> should simply *replace* foldl with the new fold. Otherwise we should
> get rid of the new List.fold.
for short: I have no objections to get rid of fol
Hi Stefan,
> They were removed from the pred_set_conv database a while ago by Florian
>
> http://isabelle.in.tum.de/repos/isabelle/rev/7f9e05b3d0fb
>
> because they were considered "potentially dangerous", but now that sets
> and predicates can be distinguished again, this rule (and the dual r
On 13.01.2012 13:49, Lars Noschinski wrote:
Hi,
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the status is displayed as "startup". In
particular, no parsing, syntax coloring or pro
On Thu, 12 Jan 2012, Lukas Bulwahn wrote:
On 01/11/2012 09:29 PM, Alexander Krauss wrote:
The real problem is in fact JinjaThreads. AFAIK, the only machine at
TUM where it can still build (in principle) is lxbroy10, but as Lukas
pointed out there are still some failures, cf.
http://isabelle
Hi,
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the status is displayed as "startup". In
particular, no parsing, syntax coloring or proof checking happens; the
polyml processes
On Fri, 13 Jan 2012, Brian Huffman wrote:
I am writing about the following recent changeset, which adds another
left-fold operator to HOL/List.thy.
author haftmann
Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
changeset 46133 d9fe85d3d2cd
parent 461325a29dbf4c155
child 46134 4b9d
I agree very strongly. I am not tied to any particular argument order,
but there should only be 2, not 3 folds. And there should be no claims
of canonicity. If anything, the canonical fold operator (with some
sensible argument order) is foldr f c which replaces :: by f and [] by
c. And to avoid fur
