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

Many thanks, much appreciated, esp the inductive lemmas!


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