| Wed, 02 Feb 2005 08:53:03 +0100 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Sun, 30 Jan 2005 20:48:50 +0100 |
nipkow |
renamed a few vars, added a lemma
|
file |
diff |
annotate
|
| Fri, 28 Jan 2005 15:44:03 +0100 |
nipkow |
proof simpification
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 13:52:09 +0100 |
paulson |
new theorem image_eq_fold
|
file |
diff |
annotate
|
| Tue, 14 Dec 2004 10:45:16 +0100 |
paulson |
new and stronger lemmas and improved simplification for finite sets
|
file |
diff |
annotate
|
| Sun, 12 Dec 2004 16:25:47 +0100 |
nipkow |
REorganized Finite_Set
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 18:30:59 +0100 |
nipkow |
First step in reorganizing Finite_Set
|
file |
diff |
annotate
|
| Mon, 06 Dec 2004 14:14:03 +0100 |
nipkow |
Started to clean up and generalize FiniteSet
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 11:12:10 +0100 |
nipkow |
changed the order of !!-quantifiers in finite set induction.
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 18:58:59 +0100 |
obua |
prettier proof of setsum_diff
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 16:42:54 +0100 |
nipkow |
renamed 2 lemmas
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 15:50:27 +0100 |
obua |
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 15:25:39 +0100 |
obua |
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 09:08:35 +0100 |
nipkow |
generalized lemma
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 08:58:32 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 13 Nov 2004 07:47:34 +0100 |
nipkow |
More lemmas
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
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
|
| Mon, 09 Aug 2004 10:09:44 +0200 |
nipkow |
Aded a thm.
|
file |
diff |
annotate
|
| Wed, 04 Aug 2004 19:11:02 +0200 |
nipkow |
added some inj_on thms
|
file |
diff |
annotate
|
| Thu, 22 Jul 2004 17:37:31 +0200 |
nipkow |
Modified \<Sum> syntax a little.
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
| Wed, 14 Jul 2004 10:25:03 +0200 |
nipkow |
added {0::nat..n(} = {..n(}
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:55 +0200 |
paulson |
ringpower to recpower
|
file |
diff |
annotate
|
| Tue, 15 Jun 2004 10:40:05 +0200 |
paulson |
strengthened some theorems
|
file |
diff |
annotate
|
| Wed, 09 Jun 2004 11:18:51 +0200 |
paulson |
moved some cardinality results into main HOL
|
file |
diff |
annotate
|
| Fri, 14 May 2004 16:52:53 +0200 |
paulson |
removed a premise of card_inj_on_le
|
file |
diff |
annotate
|
| Wed, 12 May 2004 10:00:56 +0200 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|