Re: [Isarmathlib-devel] Direct product

[Slawomir Kolodynski]

Seo,
Thank you for your contribution. Very nice job. I will
include it in the next IsarMathLib release planned for
late July. It will show up on the Tiddly Formal Math
site earlier than that. I understand that you are
releasing DirectProduct_ZF.thy with the modified BSD
license, like the rest of IsarMathLib. I will write
more comments later. 

Slawek 



http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)