avoid polymorphic equality;
do not export ring_conv (which is not a conversion anyway);
renamed algebra_tac to ring_tac;
ring_tac: simplified tactic wrapper, no longer handles ERROR;
(* Title: HOL/ROOT.ML
ID: $Id$
Classical Higher-order Logic.
*)
use_thy "Main";
path_add "~~/src/HOL/Library";
Goal "True"; (*leave subgoal package empty*)