src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
19 months ago wenzelm 2017-11-26 more symbols;
2016-07-19 wenzelm 2016-07-19 misc tuning and simplification;
2016-07-19 wenzelm 2016-07-19 misc tuning and simplification;
2016-06-01 wenzelm 2016-06-01 more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;
2016-06-01 wenzelm 2016-06-01 prefer rat numberals;
2016-06-01 wenzelm 2016-06-01 tuned signature;
2016-05-31 wenzelm 2016-05-31 ad-hoc overloading for standard operations on type Rat.rat;
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-01 wenzelm 2015-06-01 eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-08 wenzelm 2014-10-08 eliminated some exotic combinators;
2014-10-08 wenzelm 2014-10-08 clarified messages depending on options; misc tuning and simplification;
2014-08-10 wenzelm 2014-08-10 reduced warnings;
2014-04-20 paulson 2014-04-20 sos accepts False, returns apply command
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-02-15 wenzelm 2014-02-15 tuned whitespace;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-09-29 wenzelm 2013-09-29 backout c6297fa1031a -- strange parsers are required to make this work;
2013-09-28 wenzelm 2013-09-28 proper wrapper for parser -- more explicit error;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
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-08-24 huffman 2011-08-24 delete commented-out dead code
2011-08-22 huffman 2011-08-22 comment out dead code to avoid compiler warnings
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-01-10 wenzelm 2011-01-10 eliminated obsolete LargeInt -- Int is unbounded;
2011-01-08 wenzelm 2011-01-08 renamed Sum_Of_Squares to Sum_of_Squares;