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