# HG changeset patch
# User chaieb
# Date 1093869618 -7200
# Node ID a1e84e86c583e98969dfe8209bfffa1841d283e6
# Parent  5d7c96e0f9dcde3f135a836c4f5537f94fbd3e80
corrected

diff -r 5d7c96e0f9dc -r a1e84e86c583 src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 14:40:18 2004 +0200
@@ -24,12 +24,6 @@
   val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
-  val timef : (unit->thm) -> thm
-  val prtime : unit -> unit
-  val time_reset  : unit -> unit
-  val timef2 : (unit->thm) -> thm
-  val prtime2 : unit -> unit
-  val time_reset2  : unit -> unit
 end;
 
 structure CooperProof : COOPER_PROOF =
@@ -879,8 +873,8 @@
 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
 (* ------------------------------------------------------------------------- *)
 
-val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
-val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
+(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
+(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
 
 fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    (* lfm_thm : efm = linearized form of efm*)
@@ -913,16 +907,19 @@
    val dlcm = mk_numeral (divlcm x cfm)
    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    val cms = if ((length A) < (length B )) then "pi" else "mi"
-   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
+(*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
    (* synthesize the proof of cooper's theorem*)
     (* cp_thm: EX x. cfm = Q*)
-   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
+   val cp_thm =  cooper_thm sg cms x cfm dlcm A B
    (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+(*
    val _ = prth cp_thm
    val _ = writeln "Expanding the bounded EX..."
-   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
-   val _ = writeln "Expanded"
+*)
+   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
+(*
+   val _ = writeln "Expanded" *)
    (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    val (lsuth,rsuth) = qe_get_terms (uth)
    (* lseacth = EX x. efm; rseacth = EX x. fm*)
diff -r 5d7c96e0f9dc -r a1e84e86c583 src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Aug 30 14:40:18 2004 +0200
@@ -24,12 +24,6 @@
   val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
-  val timef : (unit->thm) -> thm
-  val prtime : unit -> unit
-  val time_reset  : unit -> unit
-  val timef2 : (unit->thm) -> thm
-  val prtime2 : unit -> unit
-  val time_reset2  : unit -> unit
 end;
 
 structure CooperProof : COOPER_PROOF =
@@ -879,8 +873,8 @@
 (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
 (* ------------------------------------------------------------------------- *)
 
-val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
-val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
+(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
+(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
 
 fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    (* lfm_thm : efm = linearized form of efm*)
@@ -913,16 +907,19 @@
    val dlcm = mk_numeral (divlcm x cfm)
    (* Which set is smaller to generate the (hoepfully) shorter proof*)
    val cms = if ((length A) < (length B )) then "pi" else "mi"
-   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
+(*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
    (* synthesize the proof of cooper's theorem*)
     (* cp_thm: EX x. cfm = Q*)
-   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
+   val cp_thm =  cooper_thm sg cms x cfm dlcm A B
    (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+(*
    val _ = prth cp_thm
    val _ = writeln "Expanding the bounded EX..."
-   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
-   val _ = writeln "Expanded"
+*)
+   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
+(*
+   val _ = writeln "Expanded" *)
    (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    val (lsuth,rsuth) = qe_get_terms (uth)
    (* lseacth = EX x. efm; rseacth = EX x. fm*)