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

On Fri, Jun 13, 2008 at 10:38, Lawrence Paulson <lp15 at> wrote:
> Blast doesn't look like the right tool for this problem.
> You can prove it like this:
>   lemma
>   "noBot LNil = True" unfolding noBot_def
>     by (simp add: finlsts_rec_LNil)

I had the same thought, but I tried:

    "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?


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