src/HOL/Integ/cooper_proof.ML
changeset 16389 48832eba5b1e
parent 15661 9ef583b08647
child 17485 c39871c52977
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 04:05:15 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 09:46:35 2005 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val proof_of_evalc : Sign.sg -> term -> thm
     1.5    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
     1.6    val proof_of_linform : Sign.sg -> string list -> term -> thm
     1.7 -  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     1.8 +  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
     1.9    val prove_elementar : Sign.sg -> string -> term -> thm
    1.10    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    1.11  end;