src/HOL/Library/positivstellensatz.ML
changeset 32646 962b4354ed90
parent 32645 1cc5b24f5a01
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Sep 21 15:05:26 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 11:26:46 2009 +0200
     1.3 @@ -146,19 +146,19 @@
     1.4  type cert_conv = cterm -> thm * pss_tree
     1.5  
     1.6  val gen_gen_real_arith :
     1.7 -  Proof.context -> (Rat.rat -> Thm.cterm) * conv * conv * conv *
     1.8 +  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
     1.9     conv * conv * conv * conv * conv * conv * prover -> cert_conv
    1.10  val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
    1.11    thm list * thm list * thm list -> thm * pss_tree
    1.12  
    1.13  val gen_real_arith : Proof.context ->
    1.14 -  (Rat.rat -> Thm.cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
    1.15 +  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
    1.16  
    1.17  val gen_prover_real_arith : Proof.context -> prover -> cert_conv
    1.18  
    1.19 -val is_ratconst : Thm.cterm -> bool
    1.20 -val dest_ratconst : Thm.cterm -> Rat.rat
    1.21 -val cterm_of_rat : Rat.rat -> Thm.cterm
    1.22 +val is_ratconst : cterm -> bool
    1.23 +val dest_ratconst : cterm -> Rat.rat
    1.24 +val cterm_of_rat : Rat.rat -> cterm
    1.25  
    1.26  end
    1.27