the splitter is now defined as a functor
moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML
moved split_thm_info to Provers/splitter.ML
definined atomize via general mk_atomize
removed superfluous rot_eq_tac from simplifier.ML
HOL/simpdata.ML: renamed mk_meta_eq to meta_eq,
re-renamed mk_meta_eq_simp to mk_meta_eq
added Eps_eq to simpset
List = FOL +
types list 1
arities list :: (term)term
consts Nil :: "'a list"
Cons :: "['a, 'a list] => 'a list"
end