Re: [isabelle-dev] Isabelle and AFP

Florian, Amongst the set/pred emails this one doesn't seem to have garnered much response: On 17/08/2011, at 9:18 PM, Florian Haftmann wrote: I repeatedly stumble over duplication among the Isabelle distribution and the AFP [..] I too would be keen to see some way of moving reusable

[isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

Hi, Can someone please apply the attached patch to Isabelle for me? It does three things: - generalises Imperative_Quicksort to work on linearly-ordered, heap-representable types, and not just nat - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist - mildly weakens the

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

… and this time with the patch … > On 15 Nov 2015, at 22:15, Peter Gammie <pete...@gmail.com> wrote: > > Hi, > > Can someone please apply the attached patch to Isabelle for me? > > It does three things: > - generalises Imperative_Quicksort to work on linearly-

[isabelle-dev] extra lemmas

Can someone add these in at the obvious places? thanks, peter lemma LeastI2_wellorder_ex: assumes "\x::'a::wellorder. P x" and "\a. \ P a; \b. P b \ a \ b \ \ Q a" shows "Q (Least P)" using assms by clarify (blast intro!: LeastI2_wellorder) lemma fcomp_comp: "fcomp f g = comp g f" by

Re: [isabelle-dev] test failed (Archive of Formal Proofs)

On 17 Nov 2015, at 22:50, Lars Hupel wrote: > >> The email claims that this build includes my patch. > > according to the log the AFP id is e6d87060e398, which doesn't include > your patch (82552632a098). Or are you talking about another patch? Nope, that’s the one. Thanks!

Re: [isabelle-dev] test failed (Archive of Formal Proofs)

The email claims that this build includes my patch. The log says: > Running ConcurrentGC ... > ConcurrentGC: theory Model > ConcurrentGC: theory Tactics > ConcurrentGC: theory Proofs_basis > ConcurrentGC: theory TSO > ConcurrentGC: theory Handshakes > ConcurrentGC: theory MarkObject >

Re: [isabelle-dev] Future of isatest/afptest

On 19 Nov 2015, at 00:18, Lars Hupel wrote: > > […] Lars, that all sounds awesome. Reckon you could make the status of the builds somehow public? (Right now I don’t know whether my patch to ConcurrentGC works or not, because I only get failure emails and don’t know when a