src/HOL/Library/positivstellensatz.ML
changeset 70299 83774d669b51
parent 70159 57503fe1b0ff