src/HOL/Library/positivstellensatz.ML
changeset 45654 cf10bde35973
parent 44454 6f28f96a09bf
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:06:59 2011 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Nov 27 23:10:19 2011 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4  val pth_square = @{lemma "x * x >= (0::real)"  by simp};
     1.5  
     1.6  val weak_dnf_simps =
     1.7 -  List.take (simp_thms, 34) @
     1.8 +  List.take (@{thms simp_thms}, 34) @
     1.9      @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
    1.10        "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
    1.11  
    1.12 @@ -351,7 +351,8 @@
    1.13         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
    1.14         absconv1,absconv2,prover) = 
    1.15  let
    1.16 - 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.17 + val pre_ss = HOL_basic_ss addsimps
    1.18 +  @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
    1.19   val prenex_ss = HOL_basic_ss addsimps prenex_simps
    1.20   val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
    1.21   val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)