src/HOL/Hyperreal/Poly.thy
Tue, 18 Mar 2008 20:33:31 +0100 wenzelm removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
Tue, 23 Oct 2007 13:10:19 +0200 paulson random tidying of proofs
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:33 +0200 chaieb fixed proofs
Thu, 27 Sep 2007 17:55:28 +0200 paulson removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
Mon, 25 Jun 2007 15:19:34 +0200 nipkow removed redundant lemma
Mon, 11 Jun 2007 11:06:04 +0200 chaieb tuned Proof
Thu, 07 Jun 2007 02:34:37 +0200 huffman tuned
Tue, 05 Jun 2007 16:32:16 +0200 chaieb Polynomials now only depend on Deriv; Definition of degree changed
Wed, 16 May 2007 23:03:45 +0200 huffman minimize imports
Thu, 26 Apr 2007 14:24:08 +0200 wenzelm eliminated unnamed infixes, tuned syntax;
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Mon, 09 Oct 2006 02:19:51 +0200 wenzelm attribute symmetric: zero_var_indexes;
Sat, 30 Sep 2006 17:10:55 +0200 huffman add type annotations for DERIV
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Sun, 30 Jul 2006 05:53:10 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 02 Jun 2006 23:22:29 +0200 wenzelm misc cleanup;
Thu, 05 Jan 2006 22:29:55 +0100 wenzelm replaced swap by contrapos_np;
Wed, 28 Sep 2005 11:14:26 +0200 paulson new lemma
Fri, 29 Jul 2005 19:47:27 +0200 avigad changed import to Ln
Wed, 27 Jul 2005 11:28:18 +0200 paulson removed the dependence on abs_mult
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Fri, 05 Mar 2004 15:18:59 +0100 paulson Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
Fri, 16 Nov 2001 18:24:11 +0100 paulson even more theories from Jacques
less more (0) tip