Re: [isabelle] On the use of the rule HOL.refl(exive)



The two terms are not identical. Each instance of Empty in len Empty has a separate type.
Larry Paulson


On 27 Sep 2011, at 14:29, Alfio Martini wrote:

> In the script bellow, I was expecting to solve lemmas 01 and  04 directly by
> reflexivity of equality, like the
> other ones, since both terms are the same.. But the simplifier tells me
> that I have to use also the equation len01, to substitute len(Empty) for Z.
> What (basic fact) am I missing here?






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