Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
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
Fri, 28 Jan 2005 15:44:03 +0100 nipkow proof simpification file | diff | annotate
Fri, 21 Jan 2005 13:52:09 +0100 paulson new theorem image_eq_fold file | diff | annotate
Tue, 14 Dec 2004 10:45:16 +0100 paulson new and stronger lemmas and improved simplification for finite sets file | diff | annotate
Sun, 12 Dec 2004 16:25:47 +0100 nipkow REorganized Finite_Set file | diff | annotate
Thu, 09 Dec 2004 18:30:59 +0100 nipkow First step in reorganizing Finite_Set file | diff | annotate
Mon, 06 Dec 2004 14:14:03 +0100 nipkow Started to clean up and generalize FiniteSet file | diff | annotate
Wed, 24 Nov 2004 11:12:10 +0100 nipkow changed the order of !!-quantifiers in finite set induction. file | diff | annotate
Tue, 23 Nov 2004 18:58:59 +0100 obua prettier proof of setsum_diff file | diff | annotate
Tue, 23 Nov 2004 16:42:54 +0100 nipkow renamed 2 lemmas file | diff | annotate
Tue, 23 Nov 2004 15:50:27 +0100 obua relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring file | diff | annotate
Tue, 23 Nov 2004 15:25:39 +0100 obua Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff file | diff | annotate
Tue, 23 Nov 2004 09:08:35 +0100 nipkow generalized lemma file | diff | annotate
Tue, 23 Nov 2004 08:58:32 +0100 nipkow added lemma file | diff | annotate
Sat, 13 Nov 2004 07:47:34 +0100 nipkow More lemmas file | diff | annotate
Thu, 07 Oct 2004 15:42:30 +0200 paulson simplification tweaks for better arithmetic reasoning file | diff | annotate
Mon, 04 Oct 2004 15:28:03 +0200 paulson revised simprules for division file | diff | annotate
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports file | diff | annotate
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax. file | diff | annotate
Mon, 09 Aug 2004 10:09:44 +0200 nipkow Aded a thm. file | diff | annotate
Wed, 04 Aug 2004 19:11:02 +0200 nipkow added some inj_on thms file | diff | annotate
Thu, 22 Jul 2004 17:37:31 +0200 nipkow Modified \<Sum> syntax a little. file | diff | annotate
Thu, 15 Jul 2004 15:32:32 +0200 paulson redefining sumr to be a translation to setsum file | diff | annotate
Wed, 14 Jul 2004 10:25:03 +0200 nipkow added {0::nat..n(} = {..n(} file | diff | annotate
Thu, 24 Jun 2004 17:52:55 +0200 paulson ringpower to recpower file | diff | annotate
Tue, 15 Jun 2004 10:40:05 +0200 paulson strengthened some theorems file | diff | annotate
Wed, 09 Jun 2004 11:18:51 +0200 paulson moved some cardinality results into main HOL file | diff | annotate
Fri, 14 May 2004 16:52:53 +0200 paulson removed a premise of card_inj_on_le file | diff | annotate
Wed, 12 May 2004 10:00:56 +0200 nipkow fixed latex problems file | diff | annotate
Tue, 11 May 2004 20:11:08 +0200 obua changes made due to new Ring_and_Field theory file | diff | annotate
Fri, 23 Apr 2004 20:48:28 +0200 wenzelm tuned notation; file | diff | annotate
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output file | diff | annotate
Thu, 01 Apr 2004 10:54:32 +0200 paulson new type class abelian_group file | diff | annotate
Thu, 25 Mar 2004 10:32:21 +0100 paulson new material from Avigad file | diff | annotate
Wed, 10 Mar 2004 10:34:49 +0100 paulson strengthened the axclass claims file | diff | annotate
Mon, 08 Mar 2004 11:12:06 +0100 paulson generic theorems about exponentials; general tidying up file | diff | annotate
Thu, 04 Mar 2004 12:06:07 +0100 paulson new material from Avigad, and simplified treatment of division by 0 file | diff | annotate
Sat, 27 Dec 2003 21:02:14 +0100 paulson re-organized numeric lemmas file | diff | annotate
Fri, 19 Dec 2003 04:28:45 +0100 nipkow *** empty log message *** file | diff | annotate
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying file | diff | annotate
Thu, 20 Feb 2003 11:10:24 +0100 paulson new inverse image lemmas file | diff | annotate
Fri, 29 Nov 2002 09:48:28 +0100 nipkow added a few lemmas file | diff | annotate
Thu, 28 Nov 2002 10:50:42 +0100 ballarin HOL-Algebra partially ported to Isar. file | diff | annotate
Wed, 13 Nov 2002 15:24:42 +0100 berghofe Transitive closure is now defined inductively as well. file | diff | annotate
Fri, 27 Sep 2002 16:44:50 +0200 paulson Proof tidying file | diff | annotate
Fri, 20 Sep 2002 11:48:35 +0200 paulson less use of x-symbols file | diff | annotate
Mon, 12 Aug 2002 17:48:15 +0200 nipkow Added Mi and Max on sets, hid Min and Pls on numerals. file | diff | annotate
Wed, 24 Jul 2002 22:15:55 +0200 wenzelm simplified locale predicates; file | diff | annotate
Fri, 19 Jul 2002 18:44:36 +0200 wenzelm accomodate cumulative locale predicates; file | diff | annotate
Thu, 18 Jul 2002 12:08:45 +0200 wenzelm ACe_axioms; file | diff | annotate
Tue, 16 Jul 2002 18:26:09 +0200 wenzelm adapted to locale defs; file | diff | annotate
Mon, 25 Feb 2002 20:48:14 +0100 wenzelm clarified syntax of ``long'' statements: fixes/assumes/shows; file | diff | annotate
Fri, 11 Jan 2002 14:44:58 +0100 wenzelm lemmas (in ACe) AC; file | diff | annotate
Thu, 10 Jan 2002 01:10:58 +0100 wenzelm qualified exports from locales; file | diff | annotate
Thu, 06 Dec 2001 00:38:55 +0100 wenzelm renamed theory Finite to Finite_Set and converted; file | diff | annotate
less more (0) tip
isabelle