src/HOL/Finite_Set.thy
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Wed, 07 Apr 2010 11:05:11 +0200 Christian Urban simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
Tue, 30 Mar 2010 15:46:50 -0700 huffman simplify fold_graph proofs
Thu, 18 Mar 2010 13:59:20 +0100 blanchet merged
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Thu, 18 Mar 2010 13:56:32 +0100 haftmann added locales folding_one_(idem); various streamlining and tuning
Mon, 15 Mar 2010 15:13:07 +0100 haftmann corrected disastrous syntax declarations
Thu, 11 Mar 2010 14:38:13 +0100 haftmann moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
Wed, 10 Mar 2010 16:53:27 +0100 haftmann split off theory Big_Operators from theory Finite_Set
Thu, 04 Mar 2010 17:09:44 +0100 hoelzl Generalized setsum_cases
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 17 Feb 2010 17:57:37 +0100 hoelzl Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Mon, 08 Feb 2010 14:06:46 +0100 haftmann added lemmas involving Min, Max, uminus
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Fri, 01 Jan 2010 19:15:43 +0100 nipkow added lemmas
Thu, 17 Dec 2009 13:51:50 -0800 huffman merged
Thu, 17 Dec 2009 07:02:13 -0800 huffman add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
Thu, 17 Dec 2009 17:05:56 +0000 paulson Two new theorems about cardinality
Sat, 05 Dec 2009 20:02:21 +0100 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices
Wed, 25 Nov 2009 11:16:57 +0100 haftmann tuned
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Wed, 04 Nov 2009 10:17:43 +0100 nipkow fixed order of parameters in induction rules
Thu, 22 Oct 2009 09:27:48 +0200 nipkow inv_onto -> inv_into
Sun, 18 Oct 2009 12:07:56 +0200 nipkow merged
Sun, 18 Oct 2009 12:07:25 +0200 nipkow Inv -> inv_onto, inv abbr. inv_onto UNIV.
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 25 Sep 2009 09:50:31 +0200 haftmann merged
Wed, 23 Sep 2009 08:25:51 +0200 haftmann inf/sup_absorb are no default simp rules any longer
Tue, 22 Sep 2009 15:39:46 +0200 haftmann merged
Sat, 19 Sep 2009 07:38:03 +0200 haftmann inter and union are mere abbreviations for inf and sup
Thu, 24 Sep 2009 18:29:29 +0200 haftmann idempotency case for fold1
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
Fri, 28 Aug 2009 19:15:59 +0200 nipkow tuned proofs
Sat, 25 Jul 2009 18:44:54 +0200 haftmann adapted to localized interpretation of min/max-lattice
Mon, 20 Jul 2009 08:32:07 +0200 haftmann merged
Tue, 14 Jul 2009 15:54:19 +0200 haftmann refinement of lattice classes
Wed, 15 Jul 2009 15:09:33 +0200 nipkow More finite set induction rules
Sun, 12 Jul 2009 11:36:09 +0200 nipkow typo
Sun, 12 Jul 2009 11:25:56 +0200 nipkow resolvd conflict
Sun, 12 Jul 2009 10:14:51 +0200 nipkow More about gcd/lcm, and some cleaning up
Sat, 11 Jul 2009 21:33:01 +0200 haftmann added boolean_algebra type class; tuned lattice duals
Thu, 02 Jul 2009 21:24:32 +0200 wenzelm recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
Tue, 23 Jun 2009 15:48:55 +0100 paulson merged
Thu, 18 Jun 2009 17:14:08 +0100 paulson Removed unnecessary conditions concerning nonzero divisors
Tue, 23 Jun 2009 11:31:27 +0200 haftmann lemma finite_image_set by Jeremy Avigad
Fri, 05 Jun 2009 13:35:33 +0200 haftmann merged
Fri, 05 Jun 2009 08:06:03 +0200 haftmann merged
Thu, 04 Jun 2009 15:28:58 +0200 haftmann lemmas about basic set operations and Finite_Set.fold
Fri, 05 Jun 2009 09:54:26 +0200 nipkow new lemma
Thu, 04 Jun 2009 19:44:06 +0200 nipkow finite lemmas
Thu, 04 Jun 2009 13:26:32 +0200 nipkow A few finite lemmas
Tue, 02 Jun 2009 16:23:43 +0200 haftmann added/moved lemmas by Andreas Lochbihler
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Tue, 28 Apr 2009 15:50:30 +0200 haftmann stripped class recpower further
Fri, 03 Apr 2009 16:17:50 +0200 nipkow Finite_Set: lemma
Fri, 03 Apr 2009 09:27:31 +0200 nipkow added setsum_eq_1_iff
less more (0) -100 -60 tip