Re: [isabelle] nothing important

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

The first is indeed true.  I am not sure whether there are still
examples for that (which should affect only legacy induct_tac)-



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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