new version of IsarMathLib released
I have decided to suspend the Metamath to Isabelle/ZF translation and do some native Isabelle/ZF development for a change.The next long term goal is to add integration to IsarMathLib. It seems that the integral most often formalized is the gauge integral . This is a reason good enough to try something else. Searching for alternatives I found an interesting paper “Notes on Lebesgue Integration” by Gyula Lakos on a general approach to defining the Lebesgue integral. The paper constructs an integral for functions valued in a topological groups with respect to measures valued in (possibly) another topological group.
This release is the first step towards the goal of formalizing this construction.
The material added in version 1.6.0 is mostly about finite sequences (a.k.a. lists) and operations on them: concatenation, appending an element, discarding the first or last element and folding with a binary operation. This last notion is studied in the new Semigroup_ZF.thy theory where we prove some properties of products of finite sequences of semigroup elements. The development ends in a theorem that states that if 
