src/HOL/Library/comm_ring.ML
changeset 18708 4b3dadb4fe33
parent 17516 45164074dad4
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Library/comm_ring.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    val comm_ring_tac : int -> tactic
     1.5    val comm_ring_method: int -> Proof.method
     1.6    val algebra_method: int -> Proof.method
     1.7 -  val setup : (theory -> theory) list
     1.8 +  val setup : theory -> theory
     1.9  end
    1.10  
    1.11  structure CommRing: COMM_RING =
    1.12 @@ -132,11 +132,11 @@
    1.13  val algebra_method = comm_ring_method;
    1.14  
    1.15  val setup =
    1.16 -  [Method.add_method ("comm_ring",
    1.17 +  Method.add_method ("comm_ring",
    1.18       Method.no_args (comm_ring_method 1),
    1.19 -     "reflective decision procedure for equalities over commutative rings"),
    1.20 -   Method.add_method ("algebra",
    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 +     "Method for proving algebraic properties: for now only comm_ring");
    1.26  
    1.27  end;