Re: [isabelle] simp_trace_new



Your problem is purely logical and should be proved by the logical part of “auto” before simplification gets invoked.

Larry Paulson


> On 4 Dec 2014, at 16:15, Walther Neuper <wneuper at ist.tugraz.at> wrote:
> 
> Now I don't know whether
> * "auto" doesn't need the simplifier in the above proof
> * there is something I am doing wrong
> * the hint below does not yet apply to Isabelle2014.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.