Formal theory of generalization

In the article Generalization in ZF I formally define the notion of generalization in ZF set theory.

I also formalized the results of that article in the form of Isabelle proof assistant source files. You can download the Isabelle files.