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.

Larry Paulson


> On 16 Oct 2015, at 16:25, Buday Gergely <gbuday at karolyrobert.hu> wrote:
> 
> Hi,
> 
> 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 MHonArc.