Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -120 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
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
Thu, 09 Aug 2007 15:52:42 +0200 haftmann re-eliminated Option.thy file | diff | annotate
Tue, 07 Aug 2007 09:38:46 +0200 haftmann simplified proofs file | diff | annotate
Tue, 24 Jul 2007 15:20:47 +0200 haftmann using interpretation with derived concepts file | diff | annotate
Fri, 20 Jul 2007 14:27:56 +0200 haftmann simplified HOL bootstrap file | diff | annotate
Wed, 11 Jul 2007 11:00:46 +0200 berghofe Renamed inductive2 to inductive. file | diff | annotate
Tue, 10 Jul 2007 17:30:45 +0200 haftmann moved some finite lemmas here file | diff | annotate
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps file | diff | annotate
Sun, 17 Jun 2007 18:47:03 +0200 nipkow tuned laws for cancellation in divisions for fields. file | diff | annotate
Fri, 15 Jun 2007 15:10:32 +0200 nipkow made divide_self a simp rule file | diff | annotate
Thu, 14 Jun 2007 18:33:31 +0200 wenzelm tuned proofs: avoid implicit prems; file | diff | annotate
Wed, 06 Jun 2007 17:01:33 +0200 huffman generalize class constraints on some lemmas file | diff | annotate
Mon, 04 Jun 2007 15:43:30 +0200 haftmann tuned comments file | diff | annotate
Thu, 24 May 2007 08:37:39 +0200 haftmann rudimentary class target implementation file | diff | annotate
Sat, 19 May 2007 11:33:22 +0200 haftmann no special treatment in naming of locale predicates stemming form classes file | diff | annotate
Fri, 11 May 2007 20:47:30 +0200 nipkow *** empty log message *** file | diff | annotate
Fri, 11 May 2007 03:31:12 +0200 huffman generalize setsum lemmas from semiring_0_cancel to semiring_0 file | diff | annotate
Thu, 10 May 2007 10:21:46 +0200 haftmann localized Min/Max file | diff | annotate
Mon, 09 Apr 2007 21:28:24 +0200 huffman generalized type of lemma setsum_product file | diff | annotate
Tue, 20 Mar 2007 08:27:15 +0100 haftmann explizit "type" superclass file | diff | annotate
Fri, 16 Mar 2007 21:32:07 +0100 haftmann added FIXME hints file | diff | annotate
Fri, 09 Mar 2007 08:45:57 +0100 haftmann moved order on functions here file | diff | annotate
Sat, 03 Mar 2007 09:26:58 +0100 haftmann moved instance option :: finite here file | diff | annotate
Fri, 02 Mar 2007 15:43:19 +0100 haftmann added code theorems for UNIV file | diff | annotate
Wed, 14 Feb 2007 10:06:12 +0100 haftmann added class "preorder" file | diff | annotate
Wed, 07 Feb 2007 17:28:09 +0100 berghofe Adapted to new inductive definition package. file | diff | annotate
Sun, 10 Dec 2006 07:12:26 +0100 nipkow Modified lattice locale file | diff | annotate
Sat, 02 Dec 2006 11:33:08 +0100 haftmann generalized type signature of foldSet, fold file | diff | annotate
Wed, 29 Nov 2006 04:11:06 +0100 wenzelm tuned proofs; file | diff | annotate
Sat, 18 Nov 2006 00:20:16 +0100 haftmann clarified module dependencies file | diff | annotate
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation; file | diff | annotate
Wed, 08 Nov 2006 19:48:34 +0100 haftmann renamed Lattice_Locales to Lattices file | diff | annotate
Tue, 07 Nov 2006 14:03:04 +0100 haftmann made locale partial_order compatible with axclass order file | diff | annotate
Tue, 07 Nov 2006 09:33:47 +0100 krauss * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. file | diff | annotate
Tue, 04 Jul 2006 14:47:01 +0200 ballarin Method intro_locales replaced by intro_locales and unfold_locales. file | diff | annotate
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation. file | diff | annotate
Tue, 13 Jun 2006 15:07:58 +0200 paulson new results file | diff | annotate
Mon, 12 Jun 2006 22:14:38 +0200 wenzelm tuned; file | diff | annotate
Tue, 06 Jun 2006 17:07:27 +0200 paulson new lemmas concerning finite cardinalities file | diff | annotate
Tue, 02 May 2006 20:42:30 +0200 wenzelm replaced syntax/translations by abbreviation; file | diff | annotate
Sat, 08 Apr 2006 22:51:06 +0200 wenzelm refined 'abbreviation'; file | diff | annotate
Wed, 22 Mar 2006 11:14:58 +0100 nipkow translations -> abbreviations (a cool feature) file | diff | annotate
Fri, 17 Mar 2006 10:04:27 +0100 ballarin Renamed setsum_mult to setsum_right_distrib. file | diff | annotate
Thu, 22 Dec 2005 17:57:09 +0100 nipkow more lemmas file | diff | annotate
Fri, 16 Dec 2005 16:59:32 +0100 nipkow new lemmas file | diff | annotate
Fri, 07 Oct 2005 22:59:19 +0200 wenzelm replaced _K by dummy abstraction; file | diff | annotate
Tue, 04 Oct 2005 23:30:46 +0200 nipkow new lemmas file | diff | annotate
Thu, 22 Sep 2005 23:56:15 +0200 nipkow renamed rules to iprover file | diff | annotate
Tue, 30 Aug 2005 12:47:53 +0200 paulson patterns in setsum and setprod file | diff | annotate
Fri, 26 Aug 2005 10:01:06 +0200 ballarin Lemmas on dvd, power and finite summation added or strengthened. file | diff | annotate
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names file | diff | annotate
Fri, 05 Aug 2005 12:20:30 +0200 nipkow added Brian Hufmann's finite instances file | diff | annotate
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) file | diff | annotate
Fri, 08 Jul 2005 11:38:30 +0200 nipkow changed imports due to new GCD.thy file | diff | annotate
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart. file | diff | annotate
Fri, 01 Jul 2005 13:51:11 +0200 berghofe Added strong_setsum_cong and strong_setprod_cong. file | diff | annotate
Thu, 23 Jun 2005 19:40:03 +0200 nipkow fixed \<Prod> syntax file | diff | annotate
Mon, 25 Apr 2005 17:58:41 +0200 ballarin Subsumption of locale interpretations. file | diff | annotate
Thu, 21 Apr 2005 17:22:17 +0200 nipkow tuning locales file | diff | annotate
Wed, 20 Apr 2005 17:19:18 +0200 nipkow Used locale interpretations everywhere. file | diff | annotate
Tue, 19 Apr 2005 11:40:23 +0200 paulson fixed presentation file | diff | annotate
Mon, 18 Apr 2005 15:53:51 +0200 ballarin Cleaned up, now uses interpretation. file | diff | annotate
Tue, 01 Mar 2005 18:48:52 +0100 nipkow integrated Jeremy's FiniteLib file | diff | annotate
Mon, 28 Feb 2005 18:29:55 +0100 obua added setsum_diff1' which holds in more general cases than setsum_diff1 file | diff | annotate
Tue, 22 Feb 2005 10:54:30 +0100 nipkow more setsum tuning file | diff | annotate
Mon, 21 Feb 2005 19:23:46 +0100 nipkow more fine tuniung file | diff | annotate
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum file | diff | annotate
Fri, 18 Feb 2005 11:48:42 +0100 nipkow tuning file | diff | annotate
Mon, 14 Feb 2005 10:24:58 +0100 paulson simplified a proof file | diff | annotate
Thu, 10 Feb 2005 19:14:35 +0100 nipkow some stuff is now redundant. file | diff | annotate
Thu, 10 Feb 2005 16:03:18 +0100 paulson non-inductive fold1Set proofs file | diff | annotate
Thu, 10 Feb 2005 13:01:46 +0100 paulson simplified a key lemma for foldSet file | diff | annotate
Thu, 10 Feb 2005 10:43:57 +0100 berghofe Subscripts for theorem lists now start at 1. file | diff | annotate
Wed, 09 Feb 2005 18:50:09 +0100 nipkow Extracted generic lattice stuff to new Lattice_Locales.thy file | diff | annotate
Wed, 09 Feb 2005 18:32:28 +0100 paulson new foldSet proofs file | diff | annotate
Wed, 09 Feb 2005 12:08:46 +0100 paulson revised fold1 proofs file | diff | annotate
Wed, 09 Feb 2005 10:17:09 +0100 paulson revised fold1 proofs file | diff | annotate
Tue, 08 Feb 2005 18:32:34 +0100 nipkow cvs merge problem fixed file | diff | annotate
Tue, 08 Feb 2005 15:11:30 +0100 paulson new treatment of fold1 file | diff | annotate
Tue, 08 Feb 2005 09:46:00 +0100 nipkow Fixed lattice defns file | diff | annotate
Mon, 07 Feb 2005 18:20:46 +0100 nipkow *** empty log message *** file | diff | annotate
Mon, 07 Feb 2005 08:02:14 +0100 nipkow fixed latex problems file | diff | annotate
Sat, 05 Feb 2005 19:24:11 +0100 nipkow Added Lattice locale file | diff | annotate
Fri, 04 Feb 2005 18:34:34 +0100 paulson comment file | diff | annotate
Fri, 04 Feb 2005 17:14:42 +0100 nipkow Added semi-lattice locales and reorganized fold1 lemmas file | diff | annotate
Wed, 02 Feb 2005 18:06:00 +0100 paulson generalization and tidying file | diff | annotate
Wed, 02 Feb 2005 09:15:40 +0100 nipkow fold and fol1 changes file | diff | annotate
Wed, 02 Feb 2005 08:53:03 +0100 nipkow added [simp] file | diff | annotate
Sun, 30 Jan 2005 20:48:50 +0100 nipkow renamed a few vars, added a lemma file | diff | annotate
less more (0) -120 tip
isabelle