| Thu, 07 Jun 2007 17:21:43 +0200 |
obua |
deleted comments
|
file |
diff |
annotate
|
| Thu, 07 Jun 2007 14:26:05 +0200 |
obua |
deleted legacy lemmas
|
file |
diff |
annotate
|
| Thu, 07 Jun 2007 11:25:27 +0200 |
nipkow |
somebody elses problem fixed
|
file |
diff |
annotate
|
| Thu, 24 May 2007 22:55:53 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:48:24 +0200 |
huffman |
move lemmas to RealPow.thy; tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 May 2007 17:45:42 +0200 |
huffman |
added general sum-squares lemmas
|
file |
diff |
annotate
|
| Mon, 14 May 2007 09:33:18 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Mon, 14 May 2007 08:15:13 +0200 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Sun, 13 May 2007 09:23:27 +0200 |
nipkow |
Removed junk
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 21:50:08 +0200 |
huffman |
removed unnecessary premise from power_le_imp_le_base
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 07:42:12 +0200 |
huffman |
add header
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 17:05:44 +0200 |
huffman |
simplify some proofs, remove obsolete realpow_divide
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
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
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
| Wed, 18 Feb 2004 10:40:29 +0100 |
paulson |
removed obsolete theorem
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:45:35 +0100 |
paulson |
Modified real arithmetic simplification
|
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
|
| Fri, 19 Dec 2003 10:38:48 +0100 |
paulson |
minor tweaks
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
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
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 22:10:36 +0200 |
wenzelm |
intro_classes by default;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:03:39 +0200 |
wenzelm |
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
|
file |
diff |
annotate
|
| Thu, 01 Jun 2000 11:22:27 +0200 |
fleuriot |
Updated files to remove 0r and 1r from theorems in descendant theories
|
file |
diff |
annotate
|
| Wed, 10 May 2000 22:34:30 +0200 |
wenzelm |
fixed theory deps;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 18:41:32 +0200 |
paulson |
inserted Id: lines
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:29:12 +0200 |
paulson |
heavily revised by Jacques: coercions have alphabetic names;
|
file |
diff |
annotate
|