src/HOL/Library/positivstellensatz.ML
changeset 37598 893dcabf0c04
parent 37117 59cee8807c29
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Jun 28 15:32:13 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Jun 28 15:32:17 2010 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4  val prenex_simps =
     1.5    map (fn th => th RS sym)
     1.6      ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
     1.7 -      @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
     1.8 +      @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
     1.9  
    1.10  val real_abs_thms1 = @{lemma
    1.11    "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and