algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
goals_limit := 1;
add_path "J";
add_path "JVM";
add_path "BV";
add_path "Comp";
no_document use_thy "While_Combinator";
use_thy "JTypeSafe";
use_thy "Example";
use_thy "JListExample";
use_thy "JVMListExample";
use_thy "JVMDefensive";
use_thy "LBVJVM";
use_thy "BVNoTypeError";
use_thy "BVExample";
use_thy "CorrComp";
use_thy "CorrCompTp";