src/HOL/Library/positivstellensatz.ML
changeset 38801 319a28dd3564
parent 38795 848be46708dc
child 39027 e4262f9e6a4e
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:07:35 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:46:08 2010 +0200
     1.3 @@ -164,21 +164,6 @@
     1.4    thm list * thm list * thm list -> thm * pss_tree
     1.5  type cert_conv = cterm -> thm * pss_tree
     1.6  
     1.7 -val my_eqs = Unsynchronized.ref ([] : thm list);
     1.8 -val my_les = Unsynchronized.ref ([] : thm list);
     1.9 -val my_lts = Unsynchronized.ref ([] : thm list);
    1.10 -val my_proof = Unsynchronized.ref (Axiom_eq 0);
    1.11 -val my_context = Unsynchronized.ref @{context};
    1.12 -
    1.13 -val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
    1.14 -val my_numeric_eq_conv = Unsynchronized.ref no_conv;
    1.15 -val my_numeric_ge_conv = Unsynchronized.ref no_conv;
    1.16 -val my_numeric_gt_conv = Unsynchronized.ref no_conv;
    1.17 -val my_poly_conv = Unsynchronized.ref no_conv;
    1.18 -val my_poly_neg_conv = Unsynchronized.ref no_conv;
    1.19 -val my_poly_add_conv = Unsynchronized.ref no_conv;
    1.20 -val my_poly_mul_conv = Unsynchronized.ref no_conv;
    1.21 -
    1.22  
    1.23      (* Some useful derived rules *)
    1.24  fun deduct_antisym_rule tha thb = 
    1.25 @@ -362,11 +347,6 @@
    1.26         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
    1.27         absconv1,absconv2,prover) = 
    1.28  let
    1.29 - val _ = my_context := ctxt 
    1.30 - val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ; 
    1.31 -          my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ;
    1.32 -          my_poly_conv := poly_conv; my_poly_neg_conv := poly_neg_conv; 
    1.33 -          my_poly_add_conv := poly_add_conv; my_poly_mul_conv := poly_mul_conv)
    1.34   val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
    1.35   val prenex_ss = HOL_basic_ss addsimps prenex_simps
    1.36   val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
    1.37 @@ -408,7 +388,6 @@
    1.38  
    1.39    fun hol_of_positivstellensatz(eqs,les,lts) proof =
    1.40     let 
    1.41 -    val _ = (my_eqs := eqs ; my_les := les ; my_lts := lts ; my_proof := proof)
    1.42      fun translate prf = case prf of
    1.43          Axiom_eq n => nth eqs n
    1.44        | Axiom_le n => nth les n