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
List = FOL +types list 1arities list :: (term)termconsts Nil :: "'a list" Cons :: "['a, 'a list] => 'a list" end