src/HOL/Library/positivstellensatz.ML
2012-02-22 huffman 2012-02-22 tuned whitespace
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-08-22 huffman 2011-08-22 avoid warnings
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2010-05-07 krauss 2010-05-07 spelling
2010-09-02 haftmann 2010-09-02 Table.map replaces Table.map'
2010-08-27 wenzelm 2010-08-27 disposed some old debugging tools;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-06-28 haftmann 2010-06-28 explicit is better than implicit
2010-05-25 wenzelm 2010-05-25 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-07 haftmann 2010-05-07 renamed Normalizer to the more specific Semiring_Normalizer
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-05-06 haftmann 2010-05-06 former free-floating field_comp_conv now in structure Normalizer
2010-05-06 haftmann 2010-05-06 dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-05 wenzelm 2009-11-05 tuned header; use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
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