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.