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

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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