src/HOL/Finite_Set.thy
Mon, 05 Sep 2011 07:49:31 +0200 haftmann tuned
Tue, 06 Sep 2011 14:25:16 +0200 nipkow added new lemmas
Wed, 27 Jul 2011 19:34:30 +0200 hoelzl finite vimage on arbitrary domains
Sun, 17 Jul 2011 19:48:02 +0200 haftmann moving UNIV = ... equations to their proper theories
Fri, 20 May 2011 12:35:44 +0200 haftmann tuned proofs
Fri, 20 May 2011 12:07:17 +0200 haftmann point-free characterization of operations on finite sets
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Fri, 20 May 2011 08:16:56 +0200 haftmann use point-free characterization for locale fun_left_comm_idem
Sat, 14 May 2011 18:26:25 +0200 haftmann use pointfree characterisation for fold_set locale
Thu, 12 May 2011 11:03:48 +0200 haftmann more uniform naming of lemma
Thu, 07 Apr 2011 13:01:27 +0200 haftmann dropped unused lemmas; proper Isar proof
Sun, 03 Apr 2011 11:40:32 +0200 haftmann tuned proofs
Sat, 02 Apr 2011 18:07:29 +0200 haftmann tuned proof
Thu, 17 Mar 2011 09:58:13 +0100 nipkow tuned lemma
Wed, 16 Mar 2011 19:50:56 +0100 nipkow added lemmas
Fri, 21 Jan 2011 09:44:12 +0100 haftmann moved theorem
Fri, 21 Jan 2011 09:41:59 +0100 haftmann restructured theory;
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Fri, 03 Dec 2010 20:38:58 +0100 wenzelm recoded latin1 as utf8;
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding code equation for finiteness of finite types
Sun, 28 Nov 2010 15:20:51 +0100 nipkow gave more standard finite set rules simp and intro attribute
Fri, 26 Nov 2010 18:06:48 +0100 nipkow new lemma
Tue, 23 Nov 2010 14:14:17 +0100 hoelzl Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Wed, 03 Nov 2010 08:29:32 +0100 nipkow removed assumption
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 13 Aug 2010 10:51:23 +0200 haftmann import swap prevents strange failure of SML code generator for datatypes
Mon, 12 Jul 2010 11:39:27 +0200 haftmann avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Fri, 18 Jun 2010 22:40:58 +0200 nipkow added pigeonhole lemmas
Tue, 04 May 2010 10:02:43 +0200 haftmann avoid if on rhs of default simp rules
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
less more (0) -100 -60 tip