src/HOL/Big_Operators.thy
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw;
Mon, 27 Feb 2012 10:27:21 +0100 nipkow added lemma
Thu, 23 Feb 2012 20:15:49 +0100 haftmann tuned proof
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
Sun, 19 Feb 2012 15:40:58 +0100 haftmann tuned proof
Thu, 29 Dec 2011 13:41:41 +0100 haftmann qualified Finite_Set.fold
Thu, 15 Sep 2011 12:40:08 -0400 hoelzl removed further legacy rules from Complete_Lattices
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 09 Sep 2011 00:22:18 +0200 krauss added syntactic classes for "inf" and "sup"
Thu, 26 May 2011 14:12:03 +0200 hoelzl generalize setsum_cases
Fri, 20 May 2011 11:44:16 +0200 haftmann names of fold_set locales resemble name of characteristic property more closely
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Sun, 28 Nov 2010 15:20:51 +0100 nipkow gave more standard finite set rules simp and intro attribute
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
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Tue, 20 Apr 2010 17:58:34 +0200 hoelzl Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Fri, 23 Apr 2010 15:17:59 +0200 haftmann sharpened constraint (c.f. 4e7f5b22dd7d)
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, 23 Mar 2010 12:20:27 -0700 huffman sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
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:31 +0100 haftmann generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
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
less more (0) tip