src/HOL/Library/positivstellensatz.ML
changeset 52149 32b1dbda331c
parent 52049 156e12d5cb92
child 58628 fd3c96a8ca60