--- a/src/Provers/hypsubst.ML Wed Dec 05 03:12:52 2001 +0100
+++ b/src/Provers/hypsubst.ML Wed Dec 05 03:13:21 2001 +0100
@@ -261,22 +261,11 @@
Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
-(* attributes *)
-
-fun symmetric_rule thm =
- thm RS Drule.symmetric_thm handle THM _ =>
- thm RS Data.sym handle THM _ => error "Failed to apply symmetry of == or =";
-
-fun gen_symmetric x = Drule.rule_attribute (K symmetric_rule);
-
-
(* theory setup *)
val hypsubst_setup =
[Method.add_methods
[("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
- ("subst", subst_meth, "substitution")],
- Attrib.add_attributes
- [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
+ ("subst", subst_meth, "substitution")]];
end;