added Isabelle version of Bjordal's paper