src/HOL/Library/positivstellensatz.ML
changeset 69283 39044da8bb5a
parent 69064 5840724b1d71
child 69593 3dda49e08b9d