src/HOL/Library/positivstellensatz.ML
changeset 64877 31e9920a0dc1
parent 63667 24126c564d8a
child 67091 1393c2340eec