LEO-II is a standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers for natural fragments of higher-order logic such as first-order and propositional logic. Currently LEO-II cooperates with the first-order automated theorem provers E, SPASS, and Vampire.

LEO-II is implemented in Objective CAML (Version 3.09) and its problem representation language is TPTP THF.

The development of LEO-II has been supported by the EPRSC grant EP/D070511/1 at Cambridge University, England.

Source: http://www.ags.uni-sb.de/~chris/leo/index.html
—————

I post this here for two reasons. First, the LEO team includes Larry Paulson. So, this will have some connections with Isabelle.

Secondly, take a look at the EPRSC grant page. It can guide us in writing our own project grant information page.