Re: [isabelle] nothing important



On 26.07.2013 05:54, Christian Sternagel wrote:
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 ;).

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




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