--- 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;