# HG changeset patch
# User wenzelm
# Date 966501552 -7200
# Node ID 53a62fd8b2dcaec20b757712bcc1111efa69f473
# Parent  31d4a77c89d61631dea497cecc35f50d21261374
added 'symmetric' attribute;

diff -r 31d4a77c89d6 -r 53a62fd8b2dc src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Aug 17 10:38:43 2000 +0200
+++ b/src/Provers/hypsubst.ML	Thu Aug 17 10:39:12 2000 +0200
@@ -3,9 +3,11 @@
     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     Copyright   1995  University of Cambridge
 
-Tactic to substitute using (at least) the assumption x=t in the rest of the
-subgoal, and to delete (at least) that assumption.
-Original version due to Martin Coen.
+Basic equational reasoning: (hyp_)subst method and symmetric attribute.
+
+Tactic to substitute using (at least) the assumption x=t in the rest
+of the subgoal, and to delete (at least) that assumption.  Original
+version due to Martin Coen.
 
 This version uses the simplifier, and requires it to be already present.
 
@@ -252,14 +254,28 @@
   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
 
 
-(* proof method setup *)
+(* proof methods *)
 
 val subst_meth = Method.goal_args' Attrib.local_thm stac;
 val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K 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
-  [("hyp_subst", hyp_subst_meth, "substitution using an assumption (improper)"),
-   ("subst", subst_meth, "substitution")]];
+  [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
+   ("subst", subst_meth, "substitution")],
+  Attrib.add_attributes
+  [("symmetric", (gen_symmetric, gen_symmetric), "apply symmetry of == or =")]];
 
 end;