src/HOL/Library/positivstellensatz.ML
changeset 38795 848be46708dc
parent 38558 32ad17fe2b9c
child 38801 319a28dd3564
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -439,8 +439,8 @@
     1.4    val is_req = is_binop @{cterm "op =:: real => _"}
     1.5    val is_ge = is_binop @{cterm "op <=:: real => _"}
     1.6    val is_gt = is_binop @{cterm "op <:: real => _"}
     1.7 -  val is_conj = is_binop @{cterm "op &"}
     1.8 -  val is_disj = is_binop @{cterm "op |"}
     1.9 +  val is_conj = is_binop @{cterm HOL.conj}
    1.10 +  val is_disj = is_binop @{cterm HOL.disj}
    1.11    fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
    1.12    fun disj_cases th th1 th2 = 
    1.13     let val (p,q) = Thm.dest_binop (concl th)
    1.14 @@ -484,7 +484,7 @@
    1.15      val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
    1.16      val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
    1.17      val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
    1.18 -    val th' = Drule.binop_cong_rule @{cterm "op |"} 
    1.19 +    val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
    1.20       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
    1.21       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
    1.22      in Thm.transitive th th' 
    1.23 @@ -542,12 +542,12 @@
    1.24    let 
    1.25     val nnf_norm_conv' = 
    1.26       nnf_conv then_conv 
    1.27 -     literals_conv [@{term "op &"}, @{term "op |"}] [] 
    1.28 +     literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
    1.29       (Conv.cache_conv 
    1.30         (first_conv [real_lt_conv, real_le_conv, 
    1.31                      real_eq_conv, real_not_lt_conv, 
    1.32                      real_not_le_conv, real_not_eq_conv, all_conv]))
    1.33 -  fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] [] 
    1.34 +  fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
    1.35                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
    1.36          try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
    1.37    val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)