Re: [Isarmathlib-devel] Submission: Theory of generalization

[Slawomir Kolodynski]

Thank you for your contribution. I will start working on its integration into 
IsarMathLib today. Please be patient though - I have moved recently and I don't 
have much spare time.

If you don't mind, I will convert everything to the style used by IsarMathLib, 
otherwise the HTML generating software wouldn't be able to parse it. 

Slawomir Kolodynski

--- On Thu, 12/23/10, Victor Porton <address@hidden> wrote:

> From: Victor Porton <address@hidden>
> Subject: [Isarmathlib-devel] Submission: Theory of generalization
> To: address@hidden
> Date: Thursday, December 23, 2010, 3:20 PM
> I submit the following code to be
> included into IsarMathLib:
> http://www.mathematics21.org/binaries/gen/isabelle-ZF.zip
> 
> It is accompanied with informal article (which I today
> submitted to a math journal):
> http://www.mathematics21.org/binaries/gen/generalization.pdf
> http://www.mathematics21.org/generalization.html
> 
> The code is experimental but it is checked that it works
> (with an example).
> 
> In this my submission there are two little violations of
> IsarMathLib policy:
> 
> 1. Some lemmas in ZF_Addons.thy are proved using
> apply-style proofs not ISAR. That is because these lemmas
> were proved by Larry Paulson not by myself. I do not know a
> good way to transform these proofs into ISAR.
> 
> 2. Not every lemma is commented. I think this would be
> superfluous because my code refers to an informal article
> where the theory is explained in details.
> 
> I ask to forgive me these two violations and include my
> code into IsarMathLib.
> 
> Afterward we may work on redefining the theory of integers
> using my definitions.
> 
> Looking forward for your reply, 
> 
> -- 
> Victor Porton - http://portonvictor.org
> 
> _______________________________________________
> Isarmathlib-devel mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
>