LARA Isabelle Interactive Theorem Prover Isabelle Interactive Theorem Prover Web Site In SAV'08 we will use Isabelle for some exercises. Moreover, Jahob system uses Isabelle formulas as the basis for its annotation language.