Re: [isabelle] New nat induct rule in Cong.thy

Le Sun, 12 Aug 2012 01:09:39 +0200, Manuel Eberl <eberlm at> a écrit:


I noticed some strange behaviour with induction over nat before: instead
of the usual 0 and Suc, the induction cases when doing induction over a
nat were suddenly called zero and plus1 in my code, and they didn't have
"P (Suc n)" in the induction step anymore, but "P (n + 1)".

I discovered that the problem occurs only when I import Cong.thy and
that Cong.thy declares an alternative induction rule for nat with these
exact case names.

Have you tried to change the order of the import clauses? I remember I read something in Isabelle's documentation, explaining how some imports must always come last (which in turn may suggest some others have to come before the last ones).

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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