Re: [Isarmathlib-devel] IsarMathLib 1.7.0 released

[Victor Porton]

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