src/HOL/Set_Interval.thy
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 23 Dec 2018 20:51:23 +0000 haftmann more rules
Sat, 10 Nov 2018 07:57:20 +0000 haftmann replaced some ancient ASCII syntax
Mon, 05 Nov 2018 10:02:21 +0100 nipkow simplified proof, moved lemma, added lemma
Sat, 27 Oct 2018 15:30:38 +0200 nipkow moved lemmas
Thu, 25 Oct 2018 09:48:02 +0000 haftmann more and generalized lemmas
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Thu, 12 Jul 2018 17:22:39 +0100 paulson de-applying (mostly Set_Interval)
Sun, 03 Jun 2018 15:22:30 +0100 paulson infinite product material
Wed, 02 May 2018 12:47:56 +0100 paulson type class generalisations; some work on infinite products
Sun, 15 Apr 2018 08:32:31 +0000 haftmann more and generalized lemmas
Wed, 21 Mar 2018 19:39:23 +0100 haftmann prefer convention to place operation name before type name
Sat, 10 Mar 2018 19:36:59 +0000 haftmann abstract algebraic bit operations
Mon, 26 Feb 2018 07:34:05 +0100 immler moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Sat, 13 Jan 2018 09:18:54 +0000 haftmann restored naming of lemmas after corresponding constants
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Mon, 09 Oct 2017 19:10:47 +0200 haftmann tuned imports
Wed, 23 Aug 2017 18:28:56 +0200 nipkow added lemma
Tue, 25 Apr 2017 16:39:54 +0100 paulson New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
Thu, 16 Mar 2017 13:55:29 +0000 paulson Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
Wed, 04 Jan 2017 16:18:50 +0000 paulson Many new theorems, and more tidying
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 30 Sep 2016 14:05:51 +0100 paulson new material on paths, etc. Also rationalisation
Thu, 22 Sep 2016 00:12:17 +0200 wenzelm raw control symbols are superseded by Latex.embed_raw;
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
Thu, 15 Sep 2016 14:14:49 +0100 paulson simple new lemmas, mostly about sets
Thu, 25 Aug 2016 15:50:43 +0200 Manuel Eberl More analysis lemmas
Fri, 22 Jul 2016 11:00:43 +0200 wenzelm tuned proofs -- avoid unstructured calculation;
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Fri, 27 May 2016 23:35:13 +0200 wenzelm tuned proofs;
Mon, 23 May 2016 15:33:24 +0100 paulson Lots of new material for multivariate analysis
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Fri, 01 Apr 2016 16:15:31 +0200 wenzelm explicit property for unbreakable block;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Mon, 22 Feb 2016 14:37:56 +0000 paulson An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
Tue, 09 Feb 2016 06:39:31 +0100 hoelzl instantiate topologies for nat, int and enat
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 11 Jan 2016 16:38:39 +0100 eberlm Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 29 Oct 2015 15:40:52 +0100 eberlm added many small lemmas about setsum/setprod/powr/...
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Tue, 28 Jul 2015 16:16:13 +0100 paulson the Cauchy integral theorem and related material
Mon, 20 Jul 2015 23:12:50 +0100 paulson new material for multivariate analysis, etc.
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 30 Jun 2015 13:56:16 +0100 paulson Useful lemmas. The theorem concerning swapping the variables in a double integral.
less more (0) -100 -60 tip