Re: [isabelle-dev] Problem in the AFP

2015-03-23 Thread Thiemann, Rene
Dear Peter, >> It's the operation identification phase of Autoref, >> quite difficult to debug ... I have not yet looked at it due to >> ITP-deadline. > > I found the culprit: > > summary: adapting entries to new Deriving mechanism > > in LTL_to_GBA-theory, this removes a linorder-constrai

Re: [isabelle-dev] Problem in the AFP

2015-03-23 Thread Peter Lammich
On Sa, 2015-03-21 at 18:26 +0100, Peter Lammich wrote: > It's the operation identification phase of Autoref, > quite difficult to debug ... I have not yet looked at it due to > ITP-deadline. I found the culprit: changeset: 5269:88dc498667ff user:Rene Thiemann date:Fri Mar 13 1