algebra method added.
authorchaieb
Tue Sep 20 10:36:33 2005 +0200 (2005-09-20)
changeset 174995274ecba8fea
parent 17498 d83af87bbdc5
child 17500 964bad535ac6
algebra method added.
src/HOL/Tools/comm_ring.ML
     1.1 --- a/src/HOL/Tools/comm_ring.ML	Tue Sep 20 08:24:18 2005 +0200
     1.2 +++ b/src/HOL/Tools/comm_ring.ML	Tue Sep 20 10:36:33 2005 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val comm_ring_tac : int -> tactic
     1.6    val comm_ring_method: int -> Proof.method
     1.7 +  val algebra_method: int -> Proof.method
     1.8    val setup : (theory -> theory) list
     1.9  end
    1.10  
    1.11 @@ -128,10 +129,14 @@
    1.12  
    1.13  fun comm_ring_method i = Method.METHOD (fn facts =>
    1.14    Method.insert_tac facts 1 THEN comm_ring_tac i);
    1.15 +val algebra_method = comm_ring_method;
    1.16  
    1.17  val setup =
    1.18    [Method.add_method ("comm_ring",
    1.19       Method.no_args (comm_ring_method 1),
    1.20 -     "reflective decision procedure for equalities over commutative rings")];
    1.21 +     "reflective decision procedure for equalities over commutative rings"),
    1.22 +   Method.add_method ("algebra",
    1.23 +     Method.no_args (algebra_method 1),
    1.24 +     "Method for proving algebraic properties: for now only comm_ring")];
    1.25  
    1.26  end;