| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 23:30:46 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Tue, 30 Aug 2005 12:47:53 +0200 |
paulson |
patterns in setsum and setprod
|
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
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Fri, 05 Aug 2005 12:20:30 +0200 |
nipkow |
added Brian Hufmann's finite instances
|
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
|
| Fri, 08 Jul 2005 11:38:30 +0200 |
nipkow |
changed imports due to new GCD.thy
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 13:51:11 +0200 |
berghofe |
Added strong_setsum_cong and strong_setprod_cong.
|
file |
diff |
annotate
|
| Thu, 23 Jun 2005 19:40:03 +0200 |
nipkow |
fixed \<Prod> syntax
|
file |
diff |
annotate
|
| Mon, 25 Apr 2005 17:58:41 +0200 |
ballarin |
Subsumption of locale interpretations.
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 17:22:17 +0200 |
nipkow |
tuning locales
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 17:19:18 +0200 |
nipkow |
Used locale interpretations everywhere.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 11:40:23 +0200 |
paulson |
fixed presentation
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 15:53:51 +0200 |
ballarin |
Cleaned up, now uses interpretation.
|
file |
diff |
annotate
|
| Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
file |
diff |
annotate
|
| Mon, 28 Feb 2005 18:29:55 +0100 |
obua |
added setsum_diff1' which holds in more general cases than setsum_diff1
|
file |
diff |
annotate
|
| Tue, 22 Feb 2005 10:54:30 +0100 |
nipkow |
more setsum tuning
|
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, 18 Feb 2005 11:48:42 +0100 |
nipkow |
tuning
|
file |
diff |
annotate
|
| Mon, 14 Feb 2005 10:24:58 +0100 |
paulson |
simplified a proof
|
file |
diff |
annotate
|
| Thu, 10 Feb 2005 19:14:35 +0100 |
nipkow |
some stuff is now redundant.
|
file |
diff |
annotate
|
| Thu, 10 Feb 2005 16:03:18 +0100 |
paulson |
non-inductive fold1Set proofs
|
file |
diff |
annotate
|
| Thu, 10 Feb 2005 13:01:46 +0100 |
paulson |
simplified a key lemma for foldSet
|
file |
diff |
annotate
|
| Thu, 10 Feb 2005 10:43:57 +0100 |
berghofe |
Subscripts for theorem lists now start at 1.
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 18:50:09 +0100 |
nipkow |
Extracted generic lattice stuff to new Lattice_Locales.thy
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 18:32:28 +0100 |
paulson |
new foldSet proofs
|
file |
diff |
annotate
|