Re: [Isarmathlib-devel] IsarMathLib 1.7.0 released

[Victor Porton]

15.02.2011, 22:38, "Slawomir Kolodynski" <address@hidden>:
>>  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.

For me now is not important the choice of these two variants whether to work 
better or to present my theory better.

I have been coded my idea and thus my task is done. It is not much important 
how and when it will be put into complete implementation. The important thing 
that this can be done and so eventually will be done.

I've done my mission with IsarMathLib for now and am going to discontinue to 
support development of formal logic.

Note that as an (mostly) unrelated topic I also attempted to code my order and 
general topology research into an Isabelle theory but has given it up because 
Isabelle has no proper support for locales expressing dual orders and dual 
lattices (see my messages in the Isabelle mailing list where I have requested 
that kind of features to implement in the future Isabelle). It is not yet done 
and I wait for this to be accomplished after what I may probably return to 
development of IsarMathLib. For now my tasks with Isabelle are done.

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

-- 
Victor Porton - http://portonvictor.org