src/HOL/Hyperreal/NthRoot.thy
Mon, 14 May 2007 09:27:24 +0200 huffman remove redundant lemmas
Sun, 13 May 2007 20:05:42 +0200 huffman define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
Sun, 13 May 2007 04:38:24 +0200 huffman removed redundant lemmas
Tue, 08 May 2007 04:56:28 +0200 huffman add lemma real_sqrt_sum_squares_triangle_ineq
Tue, 08 May 2007 03:03:23 +0200 huffman cleaned up
Tue, 17 Apr 2007 00:55:00 +0200 huffman moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
Wed, 11 Apr 2007 03:54:53 +0200 huffman move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
Wed, 14 Mar 2007 21:52:26 +0100 huffman move sqrt_divide_self_eq to NthRoot.thy
Sat, 16 Dec 2006 20:23:45 +0100 huffman moved several theorems; rearranged theory dependencies
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;
Sun, 24 Sep 2006 02:56:59 +0200 huffman move root and sqrt stuff from Transcendental to NthRoot
Tue, 12 Sep 2006 16:44:04 +0200 huffman remove extra dependency
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;
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Thu, 29 Jul 2004 16:14:42 +0200 paulson removed some [iff] declarations from RealDef.thy, concerning inequalities
Fri, 21 May 2004 21:15:10 +0200 wenzelm tuned document;
Fri, 19 Mar 2004 10:51:03 +0100 paulson conversion of Hyperreal/Lim to new-style
Tue, 27 Jan 2004 15:39:51 +0100 paulson replacing HOL/Real/PRat, PNat by the rational number development
Wed, 14 Jan 2004 00:13:04 +0100 nipkow Told linear arithmetic package about injections "real" from nat/int into real.
Fri, 09 Jan 2004 10:46:18 +0100 paulson Defining the type class "ringpower" and deleting superseded theorems for
Thu, 01 Jan 2004 10:06:32 +0100 paulson tweaking of lemmas in RealDef, RealOrd
Tue, 23 Dec 2003 18:24:16 +0100 paulson removing real_of_posnat
Tue, 23 Dec 2003 17:41:52 +0100 paulson converting Hyperreal/NthRoot to Isar
Thu, 27 Nov 2003 10:47:55 +0100 paulson Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
Thu, 15 Nov 2001 16:12:49 +0100 paulson new theories from Jacques Fleuriot
less more (0) tip