src/HOL/Library/positivstellensatz.ML
changeset 39214 49fc6c842d6c
parent 39027 e4262f9e6a4e
child 39920 7479334d2c90