| Thu, 29 Sep 2005 15:31:34 +0200 |
nipkow |
Added a few lemmas
|
file |
diff |
annotate
|
| Fri, 26 Aug 2005 10:01:06 +0200 |
ballarin |
Lemmas on dvd, power and finite summation added or strengthened.
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 27 May 2005 16:24:48 +0200 |
ballarin |
Locale expressions: rename with optional mixfix syntax.
|
file |
diff |
annotate
|
| Mon, 23 May 2005 19:39:45 +0200 |
nipkow |
tuned setsum rewrites
|
file |
diff |
annotate
|
| Mon, 23 May 2005 11:06:41 +0200 |
nipkow |
simplifier trace info; Suc-intervals
|
file |
diff |
annotate
|
| Mon, 02 May 2005 18:59:50 +0200 |
nipkow |
turned 2 lemmas into simp rules
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
| Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Fri, 17 Dec 2004 10:15:46 +0100 |
paulson |
removed two looping simplifications in SetInterval.thy; deleted the .ML file
|
file |
diff |
annotate
|
| Sun, 12 Dec 2004 16:25:47 +0100 |
nipkow |
REorganized Finite_Set
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|