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



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

Hallo,

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.