| 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 |
| 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 |