# HG changeset patch
# User paulson
# Date 938084979 -7200
# Node ID ae28545cd104229d69938b92b1d3a4187ed1ffa7
# Parent  dca904d4ce4c387763e3257b801db644218fd86d
The restrict_to_left rule fixes some bugs

diff -r dca904d4ce4c -r ae28545cd104 src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Thu Sep 23 13:07:25 1999 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Thu Sep 23 13:09:39 1999 +0200
@@ -19,6 +19,7 @@
   val T			: typ		(*the type of group elements*)
 
   val zero		: term
+  val restrict_to_left  : thm
   val add_cancel_21	: thm
   val add_cancel_end	: thm
   val add_left_cancel	: thm
@@ -60,10 +61,10 @@
  (*Cancel corresponding terms on the two sides of the equation, NOT on
    the same side!*)
  val cancel_ss = 
-     Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
-                      Data.cancel_simps;
+   Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
+                    (map (fn th => th RS restrict_to_left) Data.cancel_simps);
 
- val inverse_ss = Data.ss addsimps Data.add_inverses;
+ val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps;
 
  fun mk_sum []  = Data.zero
    | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;