There is also a formalisation of Lebesgue integration in the directory HOL/Probability. Larry Paulson On 14 Feb 2011, at 03:32, li yongjian wrote: > Dear Isabelle users: > I'm interested in the formalization of integration theory in > Isabelle. > I found Stefan Richter's work in AFP. > But I cannot find any other work. > Who can do me a favor of telling me some other ork.