# HG changeset patch
# User wenzelm
# Date 1392391649 -3600
# Node ID b389f65edc44ab9ca7b04cf7355ee537fb444512
# Parent  009b71c1ed23cfcd885d304daa03fb79122a9819
removed dead code;

diff -r 009b71c1ed23 -r b389f65edc44 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 14 16:25:30 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 14 16:27:29 2014 +0100
@@ -4,16 +4,12 @@
 
 signature COOPER_TAC =
 sig
-  val trace: bool Unsynchronized.ref
   val linz_tac: Proof.context -> bool -> int -> tactic
 end
 
 structure Cooper_Tac: COOPER_TAC =
 struct
 
-val trace = Unsynchronized.ref false;
-fun trace_msg s = if !trace then tracing s else ();
-
 val cooper_ss = simpset_of @{context};
 
 val nT = HOLogic.natT;
@@ -21,15 +17,11 @@
 
 val zdvd_int = @{thm zdvd_int};
 val zdiff_int_split = @{thm zdiff_int_split};
-val all_nat = @{thm all_nat};
-val ex_nat = @{thm ex_nat};
 val split_zdiv = @{thm split_zdiv};
 val split_zmod = @{thm split_zmod};
 val mod_div_equality' = @{thm mod_div_equality'};
 val split_div' = @{thm split_div'};
 val Suc_eq_plus1 = @{thm Suc_eq_plus1};
-val imp_le_cong = @{thm imp_le_cong};
-val conj_le_cong = @{thm conj_le_cong};
 val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
 val mod_add_eq = @{thm mod_add_eq} RS sym;