| Sun, 20 May 2007 10:13:06 +0200 |
huffman |
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
|
file |
diff |
annotate
|
| Sun, 20 May 2007 09:21:04 +0200 |
huffman |
add realpow_pos_nth2 back in
|
file |
diff |
annotate
|
| Sun, 20 May 2007 09:05:44 +0200 |
huffman |
add odd_real_root lemmas
|
file |
diff |
annotate
|
| Sun, 20 May 2007 08:00:48 +0200 |
huffman |
change premises of DERIV_inverse_function lemma
|
file |
diff |
annotate
|
| Sun, 20 May 2007 03:19:42 +0200 |
huffman |
add lemmas about continuity and derivatives of roots
|
file |
diff |
annotate
|
| Fri, 18 May 2007 17:35:07 +0200 |
huffman |
Prove existence of nth roots using Intermediate Value Theorem
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:03:25 +0200 |
huffman |
tuned
|
file |
diff |
annotate
|
| Mon, 14 May 2007 09:27:24 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sun, 13 May 2007 04:38:24 +0200 |
huffman |
removed redundant lemmas
|
file |
diff |
annotate
|
| Tue, 08 May 2007 04:56:28 +0200 |
huffman |
add lemma real_sqrt_sum_squares_triangle_ineq
|
file |
diff |
annotate
|
| Tue, 08 May 2007 03:03:23 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 00:55:00 +0200 |
huffman |
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 03:54:53 +0200 |
huffman |
move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
|
file |
diff |
annotate
|
| Wed, 14 Mar 2007 21:52:26 +0100 |
huffman |
move sqrt_divide_self_eq to NthRoot.thy
|
file |
diff |
annotate
|
| Sat, 16 Dec 2006 20:23:45 +0100 |
huffman |
moved several theorems; rearranged theory dependencies
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:51 +0200 |
wenzelm |
attribute symmetric: zero_var_indexes;
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 02:56:59 +0200 |
huffman |
move root and sqrt stuff from Transcendental to NthRoot
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 16:44:04 +0200 |
huffman |
remove extra dependency
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 22:29:55 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:15:10 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:51:03 +0100 |
paulson |
conversion of Hyperreal/Lim to new-style
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Wed, 14 Jan 2004 00:13:04 +0100 |
nipkow |
Told linear arithmetic package about injections "real" from nat/int into real.
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 18:24:16 +0100 |
paulson |
removing real_of_posnat
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 17:41:52 +0100 |
paulson |
converting Hyperreal/NthRoot to Isar
|
file |
diff |
annotate
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|