src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
Fri, 14 Jun 2019 08:34:27 +0000 haftmann prefer fixed simpset for proof procedure
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Thu, 01 Feb 2018 17:15:07 +0100 wenzelm clarified signature;
Thu, 01 Feb 2018 15:12:57 +0100 wenzelm tuned signature: more operations;
Thu, 01 Feb 2018 13:55:10 +0100 wenzelm clarified signature;
Wed, 31 Jan 2018 21:05:47 +0100 wenzelm proper term_ord as in HOL/Library/positivstellensatz.ML, e.g. relevant for "0 <= c & 0 <= a ==> a + bb = 1 & c <= 1 ==> bb * c * 4 <= (12::real)";
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 23 Dec 2017 19:02:11 +0100 wenzelm more symbols;
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Tue, 19 Jul 2016 16:50:39 +0200 wenzelm misc tuning and simplification;
Tue, 19 Jul 2016 16:35:51 +0200 wenzelm misc tuning and simplification;
Wed, 01 Jun 2016 19:23:18 +0200 wenzelm more adhoc overloading;
Wed, 01 Jun 2016 15:10:27 +0200 wenzelm prefer rat numberals;
Wed, 01 Jun 2016 10:45:35 +0200 wenzelm tuned signature;
Tue, 31 May 2016 21:54:10 +0200 wenzelm ad-hoc overloading for standard operations on type Rat.rat;
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Tue, 28 Jul 2015 19:49:54 +0200 wenzelm more direct access to atomic cterms;
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Mon, 01 Jun 2015 13:46:23 +0200 wenzelm eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Wed, 08 Oct 2014 17:37:20 +0200 wenzelm eliminated some exotic combinators;
Wed, 08 Oct 2014 11:50:25 +0200 wenzelm clarified messages depending on options;
Sun, 10 Aug 2014 20:45:48 +0200 wenzelm reduced warnings;
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