--- a/src/HOL/Algebra/ringsimp.ML Mon Apr 23 18:42:05 2012 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Mon Apr 23 21:44:36 2012 +0200
@@ -6,7 +6,8 @@
signature ALGEBRA =
sig
val print_structures: Proof.context -> unit
- val setup: theory -> theory
+ val attrib_setup: theory -> theory
+ val algebra_tac: Proof.context -> int -> tactic
end;
structure Algebra: ALGEBRA =
@@ -58,6 +59,7 @@
fun add_struct_thm s =
Thm.declaration_attribute
(fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+
fun del_struct s =
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
@@ -69,13 +71,4 @@
>> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)))
"theorems controlling algebra method";
-
-
-(** Setup **)
-
-val setup =
- Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
- "normalisation of algebraic structure" #>
- attrib_setup;
-
end;