# HG changeset patch
# User chaieb
# Date 1181636158 -7200
# Node ID e7f96b296453c7a9971435789d7e1459faaa30d5
# Parent  21a7433c4bd343b459118692bb7d9050ad413fa7
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification

diff -r 21a7433c4bd3 -r e7f96b296453 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Tue Jun 12 10:15:52 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Tue Jun 12 10:15:58 2007 +0200
@@ -5,7 +5,7 @@
 
 signature PRESBURGER =
  sig
-  val cooper_tac: bool -> Proof.context -> int -> Tactical.tactic
+  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> Tactical.tactic
 end;
 
 structure Presburger : PRESBURGER = 
@@ -179,20 +179,23 @@
    NONE => all_tac st
  | SOME _ => (if q then I else TRY) (rtac TrueI i) st
 
-fun cooper_tac q ctxt i = 
+fun cooper_tac elim add_ths del_ths = fn ctxt => fn i => 
+let val ss = fst (Cooper_Data.get ctxt) delsimps del_ths addsimps add_ths
+in
 nogoal_tac i 
 THEN (EVERY o (map TRY))
  [ObjectLogic.full_atomize_tac i,
   eta_beta_tac i,
-  simp_tac (fst (Cooper_Data.get ctxt)) i,
+  simp_tac ss  i,
   generalize_tac ctxt (int_nat_terms ctxt) i,
   ObjectLogic.full_atomize_tac i,
   div_mod_tac ctxt i,
   splits_tac ctxt i,
-  simp_tac (fst (Cooper_Data.get ctxt)) i,
+  simp_tac ss i,
   eta_beta_tac i,
   nat_to_int_tac ctxt i, 
   thin_prems_tac (is_relevant ctxt) i]
-THEN core_cooper_tac ctxt i THEN finish_tac q i;
+THEN core_cooper_tac ctxt i THEN finish_tac elim i
+end;
 
 end;
\ No newline at end of file