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
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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