src/HOL/Finite_Set.thy
Tue, 20 Mar 2007 08:27:15 +0100 haftmann explizit "type" superclass
Fri, 16 Mar 2007 21:32:07 +0100 haftmann added FIXME hints
Fri, 09 Mar 2007 08:45:57 +0100 haftmann moved order on functions here
Sat, 03 Mar 2007 09:26:58 +0100 haftmann moved instance option :: finite here
Fri, 02 Mar 2007 15:43:19 +0100 haftmann added code theorems for UNIV
Wed, 14 Feb 2007 10:06:12 +0100 haftmann added class "preorder"
Wed, 07 Feb 2007 17:28:09 +0100 berghofe Adapted to new inductive definition package.
Sun, 10 Dec 2006 07:12:26 +0100 nipkow Modified lattice locale
Sat, 02 Dec 2006 11:33:08 +0100 haftmann generalized type signature of foldSet, fold
Wed, 29 Nov 2006 04:11:06 +0100 wenzelm tuned proofs;
Sat, 18 Nov 2006 00:20:16 +0100 haftmann clarified module dependencies
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 08 Nov 2006 19:48:34 +0100 haftmann renamed Lattice_Locales to Lattices
Tue, 07 Nov 2006 14:03:04 +0100 haftmann made locale partial_order compatible with axclass order
Tue, 07 Nov 2006 09:33:47 +0100 krauss * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Tue, 04 Jul 2006 14:47:01 +0200 ballarin Method intro_locales replaced by intro_locales and unfold_locales.
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation.
Tue, 13 Jun 2006 15:07:58 +0200 paulson new results
Mon, 12 Jun 2006 22:14:38 +0200 wenzelm tuned;
Tue, 06 Jun 2006 17:07:27 +0200 paulson new lemmas concerning finite cardinalities
Tue, 02 May 2006 20:42:30 +0200 wenzelm replaced syntax/translations by abbreviation;
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation';
Wed, 22 Mar 2006 11:14:58 +0100 nipkow translations -> abbreviations (a cool feature)
Fri, 17 Mar 2006 10:04:27 +0100 ballarin Renamed setsum_mult to setsum_right_distrib.
Thu, 22 Dec 2005 17:57:09 +0100 nipkow more lemmas
Fri, 16 Dec 2005 16:59:32 +0100 nipkow new lemmas
Fri, 07 Oct 2005 22:59:19 +0200 wenzelm replaced _K by dummy abstraction;
Tue, 04 Oct 2005 23:30:46 +0200 nipkow new lemmas
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover
Tue, 30 Aug 2005 12:47:53 +0200 paulson patterns in setsum and setprod
Fri, 26 Aug 2005 10:01:06 +0200 ballarin Lemmas on dvd, power and finite summation added or strengthened.
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Fri, 05 Aug 2005 12:20:30 +0200 nipkow added Brian Hufmann's finite instances
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
Fri, 08 Jul 2005 11:38:30 +0200 nipkow changed imports due to new GCD.thy
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Fri, 01 Jul 2005 13:51:11 +0200 berghofe Added strong_setsum_cong and strong_setprod_cong.
Thu, 23 Jun 2005 19:40:03 +0200 nipkow fixed \<Prod> syntax
Mon, 25 Apr 2005 17:58:41 +0200 ballarin Subsumption of locale interpretations.
Thu, 21 Apr 2005 17:22:17 +0200 nipkow tuning locales
Wed, 20 Apr 2005 17:19:18 +0200 nipkow Used locale interpretations everywhere.
Tue, 19 Apr 2005 11:40:23 +0200 paulson fixed presentation
Mon, 18 Apr 2005 15:53:51 +0200 ballarin Cleaned up, now uses interpretation.
Tue, 01 Mar 2005 18:48:52 +0100 nipkow integrated Jeremy's FiniteLib
Mon, 28 Feb 2005 18:29:55 +0100 obua added setsum_diff1' which holds in more general cases than setsum_diff1
Tue, 22 Feb 2005 10:54:30 +0100 nipkow more setsum tuning
Mon, 21 Feb 2005 19:23:46 +0100 nipkow more fine tuniung
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Fri, 18 Feb 2005 11:48:42 +0100 nipkow tuning
Mon, 14 Feb 2005 10:24:58 +0100 paulson simplified a proof
Thu, 10 Feb 2005 19:14:35 +0100 nipkow some stuff is now redundant.
Thu, 10 Feb 2005 16:03:18 +0100 paulson non-inductive fold1Set proofs
Thu, 10 Feb 2005 13:01:46 +0100 paulson simplified a key lemma for foldSet
Thu, 10 Feb 2005 10:43:57 +0100 berghofe Subscripts for theorem lists now start at 1.
Wed, 09 Feb 2005 18:50:09 +0100 nipkow Extracted generic lattice stuff to new Lattice_Locales.thy
Wed, 09 Feb 2005 18:32:28 +0100 paulson new foldSet proofs
Wed, 09 Feb 2005 12:08:46 +0100 paulson revised fold1 proofs
Wed, 09 Feb 2005 10:17:09 +0100 paulson revised fold1 proofs
Tue, 08 Feb 2005 18:32:34 +0100 nipkow cvs merge problem fixed
Tue, 08 Feb 2005 15:11:30 +0100 paulson new treatment of fold1
less more (0) -100 -60 tip