--- a/src/HOL/Library/comm_ring.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Library/comm_ring.ML Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
val comm_ring_tac : int -> tactic
val comm_ring_method: int -> Proof.method
val algebra_method: int -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end
structure CommRing: COMM_RING =
@@ -132,11 +132,11 @@
val algebra_method = comm_ring_method;
val setup =
- [Method.add_method ("comm_ring",
+ Method.add_method ("comm_ring",
Method.no_args (comm_ring_method 1),
- "reflective decision procedure for equalities over commutative rings"),
- Method.add_method ("algebra",
+ "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")];
+ "Method for proving algebraic properties: for now only comm_ring");
end;