Re: [Isarmathlib-devel] IsarMathLib 1.7.0 released

[Slawomir Kolodynski]

> general theorem about
> generalization and is not specific to NatGenIntEx_ZF.thy

The reason I did that is so that I can present Generalization_ZF on the 
formalmath.org site sooner. You used a couple of Isar syntax elements that are 
currently not parsed by the html rendering application (isar2html). I modified 
your Generalization.thy (as you probably noticed) so that it is relatively easy 
for me to extend isar2html to be able to parse it. The sublocale command would 
require greater effort.
If you wish I can put this theorem back into Generalization_ZF.thy and give up 
on presenting it on formalmath.org for now. Please indicate what do you prefer.



--- On Tue, 2/15/11, Victor Porton <address@hidden> wrote:

> From: Victor Porton <address@hidden>
> Subject: Re: [Isarmathlib-devel] IsarMathLib 1.7.0 released
> To: "Slawomir Kolodynski" <address@hidden>
> Cc: address@hidden
> Date: Tuesday, February 15, 2011, 7:23 AM
> Dear Slawomir,
> 
> You in some reason moved this from Generalization_ZF.thy to
> NatGenIntEx_ZF.thy:
> 
> sublocale 
>   generalization ⊆ generalization1 small big embed
> zf_newbig zf_move
> 
> It is clearly wrong, as that is a general theorem about
> generalization and is not specific to NatGenIntEx_ZF.thy
> (which is currently only an example and also a stub to
> develop further).
> 
> 15.02.2011, 18:05, "Slawomir Kolodynski" <address@hidden>:
> > I released version 1.7.0 of IsarMathLib. This version
> adds formalized mathematics contributed by Victor Porton,
> see theories Generalization_ZF.thy and NatGenIntEx_ZF.thy.
> 
> -- 
> Victor Porton - http://portonvictor.org
>