Re: [isabelle] Extensions to the basic Isabelle/HOL theories



Many thanks, much appreciated, esp the inductive lemmas!

Tobias

Andreas Lochbihler schrieb:
> Hello Tobias,
> 
> since you asked for some lemmas, in the attached theory are some that I
> found useful and that could go into the HOL library. They all work in
> Isabelle 2009.
> 
> Andreas
> 
> Tobias Nipkow schrieb:
>> Many thanks for your input, I have already moved half your lemmas into
>> the distribution. You seem to be the only one who provides new lemmas.
>> Hence we removed isabelle-lemmas at cl.cam.ac.uk - it may even have
>> attracted spam, I cannot remember. If other people suddenly feel
>> motivated to provide additional lemmas and there is too much of it on
>> this list, this would motivate us to think again about new ways of
>> integrating your contributions.
>>
>> Tobias
>> PS I'll let you know separately what I added and how.
>>





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