# [isabelle] Mutual coinduction

Dear List,
I'm trying to figure out mutual coinduction in a development version of
Isabelle/HOL (d4b89572ae71). In particular I want to use the coinduction
scheme for two sets defined by mutual coinduction, but I'm not even able
to formulate my goal in a way that I can use 'coinduct'.
Consider the following minimal example:
theory Tmp
imports
Main
begin
coinductive_set X and Y where
"n â Y â Suc n â X"
| "n â X â Suc n â Y"
lemma tmp:
shows "(âx. P x â x â X) â (âx. Q x â x â Y)"
proof (coinduct rule: X_Y.coinduct)
sorry
end
In the first line of the proof of lemma 'tmp' the following exception is
raised
exception TERM raised (line 80 of "Isar/rule_cases.ML"):
Expected 2 binop arguments
ân. B.0 = Suc n â (Q n â n â Y)
What am I doing wrong? What is 'B.0'? I don't understand what's
happening here.
Tom

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