| Sat, 30 Sep 2006 17:10:55 +0200 |
huffman |
add type annotations for DERIV
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 05:53:10 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
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
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 19:34:22 +0200 |
huffman |
starfun, starset, and other functions on NS types are now polymorphic;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
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
|
| Tue, 28 Jun 2005 15:28:04 +0200 |
paulson |
stricter first-order check for meson
|
file |
diff |
annotate
|
| Mon, 09 May 2005 16:38:56 +0200 |
paulson |
from simplesubst to new subst
|
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
|
| Thu, 02 Dec 2004 11:42:01 +0100 |
nipkow |
Added "ALL x > y" and relatives.
|
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
|
| Fri, 01 Oct 2004 11:53:31 +0200 |
paulson |
tweaking of arithmetic proofs
|
file |
diff |
annotate
|
| Thu, 30 Sep 2004 15:43:50 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
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, 04 Aug 2004 09:44:40 +0200 |
nipkow |
fixed tex problem
|
file |
diff |
annotate
|
| Sat, 31 Jul 2004 20:54:23 +0200 |
paulson |
conversion of Hyperreal/{Fact,Filter} to Isar scripts
|
file |
diff |
annotate
|
| Fri, 30 Jul 2004 18:37:58 +0200 |
paulson |
conversion of Integration and NSPrimes to Isar scripts
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:23:40 +0200 |
paulson |
New material on integration, etc. Moving Hyperreal/ex
|
file |
diff |
annotate
|