http://isabelle.in.tum.de/testboard/Isabelle/rev/d765be00b181
There is a separate changeset for the AFP. If you’re happy with the one above, and maybe Tom sends me a rebased version, I can push them both. Gerwin On 30 Jun 2014, at 2:22 pm, Thomas Sewell <thomas.sew...@nicta.com.au> wrote: > The changeset has landed in the sense that I sent Gerwin a bundle containing: > > changeset: 6bf63b1f41f0 > tag: tip > user: Thomas Sewell <thomas.sew...@nicta.com.au> > date: Wed Jun 11 14:24:23 2014 +1000 > summary: Hypsubst preserves equality hypotheses > > He probably pushed it to the testboard with that changeset ID, but he might > have rebased, in which case it will have that summary but a different ID. I > don't know what the testboard report was, and in the meanwhile Gerwin has > been travelling, so no further progress has been made. > > I'd like to get this process moving again. If noone has any objections, I'd > like to move the change into mainline ASAP so it can be included in the > upcoming release. I can help fix any resulting failures which I've somehow > overlooked. I'm not sure who I should ask to push the change in though. > > Thomas. > > ________________________________________ > From: Makarius [makar...@sketis.net] > Sent: Monday, June 30, 2014 9:56 PM > To: Gerwin Klein; Thomas Sewell > Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de > Subject: Re: [isabelle-dev] Towards the Isabelle2014 release > > On Wed, 11 Jun 2014, Gerwin Klein wrote: > >> On 11.06.2014, at 2:56 pm, Thomas Sewell <thomas.sew...@nicta.com.au> wrote: >> >>> Gerwin will push the isabelle hypsubst change to the testboard now >>> (assuming he can remember how). >> >> He could and did. > > Has that change been landed? Which changeset IDs are relevant? > > I don't have any special expertise in this area, but merely want to make > sure that we can move on towards the release. > > > Makarius > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
