| 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
|
| Wed, 09 Feb 2005 12:08:46 +0100 |
paulson |
revised fold1 proofs
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 10:17:09 +0100 |
paulson |
revised fold1 proofs
|
file |
diff |
annotate
|
| Tue, 08 Feb 2005 18:32:34 +0100 |
nipkow |
cvs merge problem fixed
|
file |
diff |
annotate
|
| Tue, 08 Feb 2005 15:11:30 +0100 |
paulson |
new treatment of fold1
|
file |
diff |
annotate
|
| Tue, 08 Feb 2005 09:46:00 +0100 |
nipkow |
Fixed lattice defns
|
file |
diff |
annotate
|
| Mon, 07 Feb 2005 18:20:46 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 07 Feb 2005 08:02:14 +0100 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
| Sat, 05 Feb 2005 19:24:11 +0100 |
nipkow |
Added Lattice locale
|
file |
diff |
annotate
|
| Fri, 04 Feb 2005 18:34:34 +0100 |
paulson |
comment
|
file |
diff |
annotate
|
| Fri, 04 Feb 2005 17:14:42 +0100 |
nipkow |
Added semi-lattice locales and reorganized fold1 lemmas
|
file |
diff |
annotate
|
| Wed, 02 Feb 2005 18:06:00 +0100 |
paulson |
generalization and tidying
|
file |
diff |
annotate
|
| Wed, 02 Feb 2005 09:15:40 +0100 |
nipkow |
fold and fol1 changes
|
file |
diff |
annotate
|
| 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
|