# HG changeset patch
# User chaieb
# Date 1118735195 -7200
# Node ID 48832eba5b1ef6873e59c0a01b420bb42ca78dd8
# Parent  1ff571813848da29b28793648b2ca5fb3c9cf0b9
int --> IntInt.int

diff -r 1ff571813848 -r 48832eba5b1e src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Tue Jun 14 04:05:15 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Tue Jun 14 09:46:35 2005 +0200
@@ -12,21 +12,21 @@
   exception COOPER
   exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
-  val mk_numeral : int -> term
-  val dest_numeral : term -> int
+  val mk_numeral : IntInf.int -> term
+  val dest_numeral : term -> IntInf.int
   val is_numeral : term -> bool
   val zero : term
   val one : term
-  val linear_cmul : int -> term -> term
+  val linear_cmul : IntInf.int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 
   val linear_neg : term -> term
   val lint : string list -> term -> term
   val linform : string list -> term -> term
-  val formlcm : term -> term -> int
-  val adjustcoeff : term -> int -> term -> term
+  val formlcm : term -> term -> IntInf.int
+  val adjustcoeff : term -> IntInf.int -> term -> term
   val unitycoeff : term -> term -> term
-  val divlcm : term -> term -> int
+  val divlcm : term -> term -> IntInf.int
   val bset : term -> term -> term list
   val aset : term -> term -> term list
   val linrep : string list -> term -> term -> term -> term
@@ -35,7 +35,7 @@
   val simpl : term -> term
   val fv : term -> string list
   val negate : term -> term
-  val operations : (string * (int * int -> bool)) list
+  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
   val conjuncts : term -> term list
   val disjuncts : term -> term list
   val has_bound : term -> bool
@@ -65,7 +65,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 (*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
-relation operations of Type : [int,int]---> bool *) 
+relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
  
 (* ------------------------------------------------------------------------- *) 
  
@@ -85,14 +85,14 @@
  
 fun mk_numeral 0 = Const("0",HOLogic.intT)
    |mk_numeral 1 = Const("1",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
+   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
  
 (*Transform an Term to an natural number*)	  
 	  
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
-       IntInf.toInt (HOLogic.dest_binum n);
+       HOLogic.dest_binum n;
 (*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
@@ -116,7 +116,7 @@
 (* Note that we're quite strict: the ci must be present even if 1            *) 
 (* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
 (* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
-(* ------------------------------------------------------------------------- *) 
+(* ------------------------------------------------------------------------- *)  
  
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
diff -r 1ff571813848 -r 48832eba5b1e src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 04:05:15 2005 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 09:46:35 2005 +0200
@@ -21,7 +21,7 @@
   val proof_of_evalc : Sign.sg -> term -> thm
   val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
   val proof_of_linform : Sign.sg -> string list -> term -> thm
-  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
+  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
 end;
diff -r 1ff571813848 -r 48832eba5b1e src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 14 04:05:15 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 14 09:46:35 2005 +0200
@@ -12,21 +12,21 @@
   exception COOPER
   exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
-  val mk_numeral : int -> term
-  val dest_numeral : term -> int
+  val mk_numeral : IntInf.int -> term
+  val dest_numeral : term -> IntInf.int
   val is_numeral : term -> bool
   val zero : term
   val one : term
-  val linear_cmul : int -> term -> term
+  val linear_cmul : IntInf.int -> term -> term
   val linear_add : string list -> term -> term -> term 
   val linear_sub : string list -> term -> term -> term 
   val linear_neg : term -> term
   val lint : string list -> term -> term
   val linform : string list -> term -> term
-  val formlcm : term -> term -> int
-  val adjustcoeff : term -> int -> term -> term
+  val formlcm : term -> term -> IntInf.int
+  val adjustcoeff : term -> IntInf.int -> term -> term
   val unitycoeff : term -> term -> term
-  val divlcm : term -> term -> int
+  val divlcm : term -> term -> IntInf.int
   val bset : term -> term -> term list
   val aset : term -> term -> term list
   val linrep : string list -> term -> term -> term -> term
@@ -35,7 +35,7 @@
   val simpl : term -> term
   val fv : term -> string list
   val negate : term -> term
-  val operations : (string * (int * int -> bool)) list
+  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
   val conjuncts : term -> term list
   val disjuncts : term -> term list
   val has_bound : term -> bool
@@ -65,7 +65,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 (*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
-relation operations of Type : [int,int]---> bool *) 
+relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
  
 (* ------------------------------------------------------------------------- *) 
  
@@ -85,14 +85,14 @@
  
 fun mk_numeral 0 = Const("0",HOLogic.intT)
    |mk_numeral 1 = Const("1",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
+   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
  
 (*Transform an Term to an natural number*)	  
 	  
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
-       IntInf.toInt (HOLogic.dest_binum n);
+       HOLogic.dest_binum n;
 (*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
@@ -116,7 +116,7 @@
 (* Note that we're quite strict: the ci must be present even if 1            *) 
 (* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
 (* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
-(* ------------------------------------------------------------------------- *) 
+(* ------------------------------------------------------------------------- *)  
  
  
 fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
diff -r 1ff571813848 -r 48832eba5b1e src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Jun 14 04:05:15 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Jun 14 09:46:35 2005 +0200
@@ -21,7 +21,7 @@
   val proof_of_evalc : Sign.sg -> term -> thm
   val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
   val proof_of_linform : Sign.sg -> string list -> term -> thm
-  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
+  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
   val prove_elementar : Sign.sg -> string -> term -> thm
   val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
 end;