[isabelle] nothing important

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 ;).



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