Email Gateway (Aug 19 2022 at 11:22): Email Gateway (Aug 19 2022 at 11:22):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
The following comment in Nat.thy seems odd to me:
lemma nat_induct [case_names 0 Suc, induct type: nat]:
-- {* for backward compatibility -- names of variables differ *}
fixes n
assumes "P 0"
and "!!n. P n ==> P (Suc n)"
shows "P n"
using assms by (rule nat.induct)
Either I do not understand the meaning (what names are different) -- in
which case, please somebody explain -- or it is obsolete -- then please
remove ;).
cheers
chris
Email Gateway (Aug 19 2022 at 11:22):From: Lars Noschinski <noschinl@in.tum.de>
I think this is nat.induct vs. nat_induct, which only differ in the
bound variable, i.e. "nat" vs "n". There might be some really old proofs
relying on that.
-- Lars
Email Gateway (Aug 19 2022 at 11:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The first is indeed true. I am not sure whether there are still
examples for that (which should affect only legacy induct_tac)-
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC