updated sample problems, added abs axioms to builtins, added to Isabelle formalizations