src/HOL/Library/positivstellensatz.ML
changeset 37380 35815ce9218a
parent 37117 59cee8807c29
child 37598 893dcabf0c04