| 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 |
| 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 |
| Tue, 11 May 2004 20:11:08 +0200 | obua | changes made due to new Ring_and_Field theory | file | diff | annotate |
| Fri, 23 Apr 2004 20:48:28 +0200 | wenzelm | tuned notation; | file | diff | annotate |
| Wed, 14 Apr 2004 14:13:05 +0200 | kleing | use more symbols in HTML output | file | diff | annotate |
| Thu, 01 Apr 2004 10:54:32 +0200 | paulson | new type class abelian_group | file | diff | annotate |
| Thu, 25 Mar 2004 10:32:21 +0100 | paulson | new material from Avigad | file | diff | annotate |
| Wed, 10 Mar 2004 10:34:49 +0100 | paulson | strengthened the axclass claims | file | diff | annotate |
| Mon, 08 Mar 2004 11:12:06 +0100 | paulson | generic theorems about exponentials; general tidying up | file | diff | annotate |
| Thu, 04 Mar 2004 12:06:07 +0100 | paulson | new material from Avigad, and simplified treatment of division by 0 | file | diff | annotate |
| Sat, 27 Dec 2003 21:02:14 +0100 | paulson | re-organized numeric lemmas | file | diff | annotate |
| Fri, 19 Dec 2003 04:28:45 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Fri, 26 Sep 2003 10:34:57 +0200 | paulson | misc tidying | file | diff | annotate |
| Thu, 20 Feb 2003 11:10:24 +0100 | paulson | new inverse image lemmas | file | diff | annotate |
| Fri, 29 Nov 2002 09:48:28 +0100 | nipkow | added a few lemmas | file | diff | annotate |