[isabelle-dev] Problem in the AFP

Lawrence Paulson lp15 at cam.ac.uk
Sat Mar 21 23:02:36 CET 2015


I've recently pushed some changes affecting the factorial function and simplification of real expressions. 

Larry Paulson

> On 21 Mar 2015, at 17:26, Peter Lammich <lammich at in.tum.de> 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 will have look at it next week on Monday or Tuesday. Does anyone know
> the changeset that introduced the failure, or is there an easy way to
> find out?



More information about the isabelle-dev mailing list