Re: [isabelle] Recursion on finite, lazy lists (llists)
On Fri, Jun 13, 2008 at 10:38, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Blast doesn't look like the right tool for this problem.
> You can prove it like this:
> "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
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