# [isabelle] New nat induct rule in Cong.thy

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.
Is this intended behaviour? I doubt many people usually give the
explicit induction rule they want to use when doing induction over nat
(nat_induct, I think), so if they then include Cong.thy or some theory
that depends on it (like Binomial.thy), this will break all the Isar
induction proofs over nat, does it not?
Cheers,
Manuel

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