src/HOL/Library/positivstellensatz.ML
changeset 32740 9dd0a2f83429
parent 32646 962b4354ed90
child 32828 ad76967c703d
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -190,20 +190,20 @@
     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 = ref ([] : thm list);
     1.8 -val my_les = ref ([] : thm list);
     1.9 -val my_lts = ref ([] : thm list);
    1.10 -val my_proof = ref (Axiom_eq 0);
    1.11 -val my_context = ref @{context};
    1.12 +val my_eqs = Unsynchronized.ref ([] : thm list);
    1.13 +val my_les = Unsynchronized.ref ([] : thm list);
    1.14 +val my_lts = Unsynchronized.ref ([] : thm list);
    1.15 +val my_proof = Unsynchronized.ref (Axiom_eq 0);
    1.16 +val my_context = Unsynchronized.ref @{context};
    1.17  
    1.18 -val my_mk_numeric = ref ((K @{cterm True}) :Rat.rat -> cterm);
    1.19 -val my_numeric_eq_conv = ref no_conv;
    1.20 -val my_numeric_ge_conv = ref no_conv;
    1.21 -val my_numeric_gt_conv = ref no_conv;
    1.22 -val my_poly_conv = ref no_conv;
    1.23 -val my_poly_neg_conv = ref no_conv;
    1.24 -val my_poly_add_conv = ref no_conv;
    1.25 -val my_poly_mul_conv = ref no_conv;
    1.26 +val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
    1.27 +val my_numeric_eq_conv = Unsynchronized.ref no_conv;
    1.28 +val my_numeric_ge_conv = Unsynchronized.ref no_conv;
    1.29 +val my_numeric_gt_conv = Unsynchronized.ref no_conv;
    1.30 +val my_poly_conv = Unsynchronized.ref no_conv;
    1.31 +val my_poly_neg_conv = Unsynchronized.ref no_conv;
    1.32 +val my_poly_add_conv = Unsynchronized.ref no_conv;
    1.33 +val my_poly_mul_conv = Unsynchronized.ref no_conv;
    1.34  
    1.35  
    1.36      (* Some useful derived rules *)