[isabelle] coinduct problem

Hi all,

I am trying to prove a lemma by "coinduct".
I get the following error, at the point when I call  "proof coinduct"

*** exception TERM raised: Expected 3 binop arguments
*** At command "proof".

What kind of error is that? any clue?
Thanks in advance for any advice.


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