src/HOL/Tools/Presburger/cooper_dec.ML

   val divlcm : term -> term -> int
   val bset : term -> term -> term list
   val aset : term -> term -> term list
   val linrep : string list -> term -> term -> term -> term
   val list_disj : term list -> term
+  val list_conj : term list -> term
   val simpl : term -> term
   val fv : term -> string list
   val negate : term -> term
   val operations : (string * (int * int -> bool)) list
+  val conjuncts : term -> term list
+  val disjuncts : term -> term list
+  val has_bound : term -> bool
+  val minusinf : term -> term -> term
+  val plusinf : term -> term -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
 struct
 

         if is_numeral s' then (linear_cmul (dest_numeral s') t') 
         else if is_numeral t' then (linear_cmul (dest_numeral t') s') 
  
          else (warning "lint: apparent nonlinearity"; raise COOPER)
          end 
-  |_ =>   error "lint: unknown term"; 
+  |_ =>   (error "COOPER:lint: unknown term  ")
    
  
  
 (* ------------------------------------------------------------------------- *) 
 (* Linearize the atoms in a formula, and eliminate non-strict inequalities.  *)