Re: [isabelle] tracing automatic datatype theorems
This is virtually an atomic statement, so in effect you are asking for the details of how datatypes are represented internally. This representation has always been complicated, and I think the new system is even more complicated.
> On 16 Oct 2015, at 16:25, Buday Gergely <gbuday at karolyrobert.hu> wrote:
> is it possible to see the details of the proof of
> Suc n â 0
> This is an automatic proof so the proof script is not easily available I guess.
> - Gergely
This archive was generated by a fusion of
Pipermail (Mailman edition) and