The restrict_to_left rule fixes some bugs
authorpaulson
Thu Sep 23 13:09:39 1999 +0200 (1999-09-23 ago)
changeset 7586ae28545cd104
parent 7585 dca904d4ce4c
child 7587 ee0b835ca8fa
The restrict_to_left rule fixes some bugs
src/Provers/Arith/abel_cancel.ML
     1.1 --- a/src/Provers/Arith/abel_cancel.ML	Thu Sep 23 13:07:25 1999 +0200
     1.2 +++ b/src/Provers/Arith/abel_cancel.ML	Thu Sep 23 13:09:39 1999 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val T			: typ		(*the type of group elements*)
     1.5  
     1.6    val zero		: term
     1.7 +  val restrict_to_left  : thm
     1.8    val add_cancel_21	: thm
     1.9    val add_cancel_end	: thm
    1.10    val add_left_cancel	: thm
    1.11 @@ -60,10 +61,10 @@
    1.12   (*Cancel corresponding terms on the two sides of the equation, NOT on
    1.13     the same side!*)
    1.14   val cancel_ss = 
    1.15 -     Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
    1.16 -                      Data.cancel_simps;
    1.17 +   Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @ 
    1.18 +                    (map (fn th => th RS restrict_to_left) Data.cancel_simps);
    1.19  
    1.20 - val inverse_ss = Data.ss addsimps Data.add_inverses;
    1.21 + val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps;
    1.22  
    1.23   fun mk_sum []  = Data.zero
    1.24     | mk_sum tms = foldr1 (fn (x,y) => plus $ x $ y) tms;