src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
Sun, 20 Apr 2014 00:25:05 +0100 paulson sos accepts False, returns apply command
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Sat, 15 Feb 2014 21:11:29 +0100 wenzelm tuned whitespace;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Sun, 29 Sep 2013 00:15:05 +0200 wenzelm backout c6297fa1031a -- strange parsers are required to make this work;
Sat, 28 Sep 2013 16:36:17 +0200 wenzelm proper wrapper for parser -- more explicit error;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 24 Aug 2011 09:23:26 -0700 huffman delete commented-out dead code
Mon, 22 Aug 2011 16:49:45 -0700 huffman comment out dead code to avoid compiler warnings
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Mon, 10 Jan 2011 15:30:17 +0100 wenzelm eliminated obsolete LargeInt -- Int is unbounded;
Sat, 08 Jan 2011 17:39:51 +0100 wenzelm renamed Sum_Of_Squares to Sum_of_Squares;
less more (0) tip