Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
Wed, 01 Apr 2009 11:31:24 -0700 huffman generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs file | diff | annotate
Wed, 01 Apr 2009 16:03:00 +0200 nipkow added strong_setprod_cong[cong] (in analogy with setsum) file | diff | annotate
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default; file | diff | annotate
Fri, 06 Mar 2009 20:29:37 +0100 haftmann equalities for Min, Max file | diff | annotate
Wed, 04 Mar 2009 19:21:55 +0000 chaieb Added general theorems for fold_image, setsum and set_prod file | diff | annotate
Wed, 18 Feb 2009 13:39:05 +0100 haftmann reverted to previous version of Finite_Set.thy file | diff | annotate
Wed, 18 Feb 2009 11:17:29 +0000 paulson No idea what happened here! file | diff | annotate
Sun, 15 Feb 2009 22:58:02 +0100 nipkow dvd and setprod lemmas file | diff | annotate
Sun, 15 Feb 2009 16:25:16 +0100 nipkow added finite_set_choice file | diff | annotate
Sun, 15 Feb 2009 11:26:38 +0100 nipkow more finiteness file | diff | annotate
Sun, 15 Feb 2009 07:54:16 +0100 nipkow more finiteness file | diff | annotate
Sat, 14 Feb 2009 19:27:15 +0100 nipkow more finiteness file | diff | annotate
Sat, 14 Feb 2009 08:45:16 +0100 nipkow more finiteness changes file | diff | annotate
Fri, 13 Feb 2009 23:55:04 +0100 nipkow finiteness lemmas file | diff | annotate
Thu, 12 Feb 2009 18:14:43 +0100 nipkow Moved FTA into Lib and cleaned it up a little. file | diff | annotate
Tue, 03 Feb 2009 21:26:21 +0100 haftmann handling type classes without parameters file | diff | annotate
Thu, 29 Jan 2009 09:35:51 +0000 chaieb dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta file | diff | annotate
Wed, 28 Jan 2009 13:23:59 +0000 chaieb Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta file | diff | annotate
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics file | diff | annotate
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps; file | diff | annotate
Wed, 21 Jan 2009 23:40:23 +0100 haftmann changed import hierarchy file | diff | annotate
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID file | diff | annotate
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation file | diff | annotate
Thu, 11 Dec 2008 18:30:26 +0100 ballarin Conversion of HOL-Main and ZF to new locales. file | diff | annotate
Tue, 09 Dec 2008 15:31:38 -0800 huffman move lemmas from Numeral_Type.thy to other theories file | diff | annotate
Wed, 19 Nov 2008 17:54:55 +0100 nipkow Added new fold operator and renamed the old oe to fold_image. file | diff | annotate
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation file | diff | annotate
Sun, 24 Aug 2008 14:42:22 +0200 haftmann tuned import order file | diff | annotate
Tue, 15 Jul 2008 16:50:09 +0200 ballarin Removed uses of context element includes. file | diff | annotate
Tue, 01 Jul 2008 20:26:48 +0200 huffman prove lemma finite in context of finite class file | diff | annotate
Tue, 01 Jul 2008 06:51:59 +0200 huffman remove simp attribute from range_composition file | diff | annotate
Thu, 12 Jun 2008 14:10:41 +0200 nipkow Hid swap file | diff | annotate
Wed, 07 May 2008 10:56:34 +0200 berghofe - Deleted code setup for finite and card file | diff | annotate
Mon, 28 Apr 2008 20:21:11 +0200 haftmann thms Max_ge, Min_le: dropped superfluous premise file | diff | annotate
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy file | diff | annotate
Fri, 28 Mar 2008 22:00:59 +0100 haftmann only invoke interpret file | diff | annotate
Thu, 27 Mar 2008 19:04:35 +0100 haftmann no "attach UNIV" any more file | diff | annotate
Tue, 26 Feb 2008 20:38:10 +0100 haftmann tuned proofs file | diff | annotate
Wed, 06 Feb 2008 08:34:32 +0100 haftmann locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder file | diff | annotate
Fri, 07 Dec 2007 15:07:59 +0100 haftmann instantiation target rather than legacy instance file | diff | annotate
Thu, 29 Nov 2007 17:08:26 +0100 haftmann instance command as rudimentary class target file | diff | annotate
Fri, 23 Nov 2007 21:09:32 +0100 haftmann deleted card definition as code lemma; authentic syntax for card file | diff | annotate
Tue, 06 Nov 2007 08:47:25 +0100 haftmann renamed lordered_*_* to lordered_*_add_*; further localization file | diff | annotate
Fri, 26 Oct 2007 21:22:16 +0200 haftmann dropped "brown" syntax file | diff | annotate
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0 file | diff | annotate
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax file | diff | annotate
Mon, 15 Oct 2007 15:29:39 +0200 haftmann explicit parameter for class finite file | diff | annotate
Mon, 08 Oct 2007 08:04:26 +0200 haftmann clarified file | diff | annotate
Fri, 05 Oct 2007 08:38:09 +0200 nipkow added lemmas file | diff | annotate
Sat, 29 Sep 2007 08:58:51 +0200 haftmann proper syntax during class specification file | diff | annotate
Wed, 26 Sep 2007 20:27:55 +0200 haftmann moved Finite_Set before Datatype file | diff | annotate
Thu, 20 Sep 2007 16:37:28 +0200 haftmann code lemmas for cardinality file | diff | annotate
Sat, 15 Sep 2007 19:27:41 +0200 haftmann added lemmas for finiteness file | diff | annotate
Fri, 24 Aug 2007 14:21:33 +0200 paulson revised blacklisting for ATP linkup file | diff | annotate
Tue, 21 Aug 2007 13:30:36 +0200 haftmann moved ordered_ab_semigroup_add to OrderedGroup.thy file | diff | annotate
Mon, 20 Aug 2007 18:07:25 +0200 haftmann conciliated Inf/Inf_fin file | diff | annotate
Fri, 17 Aug 2007 13:58:57 +0200 haftmann dropped junk file | diff | annotate
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp file | diff | annotate
Tue, 14 Aug 2007 23:04:27 +0200 huffman minimize imports file | diff | annotate
Tue, 14 Aug 2007 23:03:42 +0200 huffman rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp] file | diff | annotate
less more (0) -100 -60 tip
isabelle