IsarMathLib version 1.6.8 released

This release is  the first version of the IsarMathLib library for the new Isabelle2009. There is a little bit of new formalized mathematics as well.

The new CommutativeSemigroup_ZF theory is another take on the subject of summing up elements of some finite subset of a semigroup. This is similar to what was done in the Semigroup theory, but this time the approach is more specific to the case when the semigroup operation is commutative and does not require a linear order on the elements that we are summing up. This formalizes the definition of where is an indexed  family of elements of the semigroup and  is some finite subset of the index set. I have  written a bit about it that previously.

I also added a couple of theorems on the notion of lifting an operation to subsets. This is just a name I came up with for the operation on subsets of that is defined naturally by any binary operation on . I discussed this in the “Interval arithmetic in groups – pass  2” post.