src/HOL/Library/positivstellensatz.ML
changeset 40217 656bb85f01ab
parent 39920 7479334d2c90
child 44058 ae85c5d64913