Re: [isabelle] Recursion on finite, lazy lists (llists)

Hi Denis,

> I had the same thought, but I tried:
>     lemma
>     "noBot LNil = True" unfolding noBot_def
>                         using finlsts_rec_LNil
>     by simp

> And it failed.  I expected to be able to substitute "using" in Isar
> for the "add:" argument to simp.  What is different?

That is, in general, not the case.  Facts chained in to simp (e.g. using
"using") are not instantiated wrt. to types, where simp rules given to
simp with add: are.

Hope this helps


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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