src/HOL/Library/positivstellensatz.ML
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-01 wenzelm 2009-10-01 moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
2009-09-30 Philipp Meyer 2009-09-30 tuned FuncFun and FuncUtil structure in positivstellensatz.ML
2009-09-22 Philipp Meyer 2009-09-22 removed opening of structures
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-22 Philipp Meyer 2009-09-22 used standard fold function and type aliases
2009-09-21 Philipp Meyer 2009-09-21 sos method generates and uses proof certificates
2009-08-26 boehmes 2009-08-26 added further conversions and conversionals
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-05-12 chaieb 2009-05-12 A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination