algebra method added.

--- a/src/HOL/Tools/comm_ring.ML	Tue Sep 20 08:24:18 2005 +0200
+++ b/src/HOL/Tools/comm_ring.ML	Tue Sep 20 10:36:33 2005 +0200
@@ -8,6 +8,7 @@
 sig
   val comm_ring_tac : int -> tactic
   val comm_ring_method: int -> Proof.method
+  val algebra_method: int -> Proof.method
   val setup : (theory -> theory) list
 end
 
@@ -128,10 +129,14 @@
 
 fun comm_ring_method i = Method.METHOD (fn facts =>
   Method.insert_tac facts 1 THEN comm_ring_tac i);
+val algebra_method = comm_ring_method;
 
 val setup =
   [Method.add_method ("comm_ring",
      Method.no_args (comm_ring_method 1),
-     "reflective decision procedure for equalities over commutative rings")];
+     "reflective decision procedure for equalities over commutative rings"),
+   Method.add_method ("algebra",
+     Method.no_args (algebra_method 1),
+     "Method for proving algebraic properties: for now only comm_ring")];
 
 end;