Tue, 07 Aug 2007 23:24:10 +0200 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 07:58:50 +0200 |
huffman |
remove simp attribute from lemma_STAR theorems
|
file |
diff |
annotate
|
Thu, 31 May 2007 23:02:16 +0200 |
huffman |
replace (- 1) with -1
|
file |
diff |
annotate
|
Tue, 22 May 2007 07:29:49 +0200 |
huffman |
rename lemmas LIM_ident, isCont_ident, DERIV_ident
|
file |
diff |
annotate
|
Thu, 17 May 2007 00:45:27 +0200 |
huffman |
cleaned up proof of Maclaurin_sin_bound
|
file |
diff |
annotate
|
Wed, 16 May 2007 23:03:45 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
Tue, 12 Dec 2006 04:31:34 +0100 |
huffman |
add type annotation
|
file |
diff |
annotate
|
Sat, 30 Sep 2006 17:10:55 +0200 |
huffman |
add type annotations for DERIV
|
file |
diff |
annotate
|
Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
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
|
Mon, 09 May 2005 16:38:56 +0200 |
paulson |
from simplesubst to new subst
|
file |
diff |
annotate
|
Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
Fri, 18 Feb 2005 11:48:53 +0100 |
nipkow |
starting to get rid of sumr
|
file |
diff |
annotate
|
Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
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
|
Wed, 28 Jul 2004 16:25:40 +0200 |
paulson |
abs notation
|
file |
diff |
annotate
|
Wed, 28 Jul 2004 10:49:29 +0200 |
paulson |
conversion of Hyperreal/MacLaurin_lemmas to Isar script
|
file |
diff |
annotate
|
Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
Fri, 16 Nov 2001 18:24:11 +0100 |
paulson |
even more theories from Jacques
|
file |
diff |
annotate
|