src/HOL/Library/positivstellensatz.ML
changeset 67951 655aa11359dc
parent 67564 d615e9ca77dc
child 69064 5840724b1d71