added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
safe_asm_more_full_simp_tac
new addss (old version retained as unsafe_addss),
new auto_tac (old version retained as unsafe_auto_tac),
clasimpset with modification functions
List = FOL +
types list 1
arities list :: (term)term
consts Nil :: "'a list"
Cons :: "['a, 'a list] => 'a list"
end