# HG changeset patch
# User chaieb
# Date 1127205393 -7200
# Node ID 5274ecba8feaf6fae31786a43a86b79df9ad44a9
# Parent  d83af87bbdc5506a5128cce38852b863f43e8ce3
algebra method added.

diff -r d83af87bbdc5 -r 5274ecba8fea src/HOL/Tools/comm_ring.ML
--- 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;