src/HOL/Topological_Spaces.thy
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 30 Dec 2018 10:34:56 +0000 haftmann prefer naming convention from datatype package for strong congruence rules
Sat, 29 Dec 2018 15:43:53 +0100 nipkow capitalize proper names in lemma names
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Sun, 21 Oct 2018 09:39:09 +0200 nipkow uniform naming of strong congruence rules
Sun, 09 Sep 2018 17:40:12 +0100 eberlm Removed problematic rules from continuous_intros
Thu, 30 Aug 2018 17:20:54 +0200 Manuel Eberl Some basic materials on filters and topology
Fri, 24 Aug 2018 20:22:14 +0000 haftmann some modernization of notation
Sat, 04 Aug 2018 01:03:39 +0200 eberlm Small lemmas about analysis
Thu, 28 Jun 2018 17:14:40 +0100 paulson Incorporating new/strengthened proofs from Library and AFP entries
Sun, 03 Jun 2018 15:22:30 +0100 paulson infinite product material
Sat, 26 May 2018 22:11:55 +0100 paulson tidying and reorganisation around Cauchy Integral Theorem
Wed, 02 May 2018 12:47:56 +0100 paulson type class generalisations; some work on infinite products
Wed, 28 Mar 2018 12:12:19 -0700 huffman tuned some proofs
Mon, 26 Mar 2018 16:12:55 +0200 Manuel Eberl Added some simple facts about limits
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
Fri, 23 Feb 2018 14:56:32 +0000 Wenda Li merged
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Thu, 08 Feb 2018 11:48:02 +0100 immler more elementary proof of connected_Times, earlier
Thu, 18 Jan 2018 15:21:06 +0100 nipkow moved t3/t4 space from AFP/Gromov to here.
Thu, 18 Jan 2018 08:08:36 +0100 nipkow more automation
Wed, 20 Dec 2017 21:06:08 +0100 nipkow tuned op's
Tue, 19 Dec 2017 13:58:12 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Tue, 10 Oct 2017 17:15:37 +0100 paulson Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
Thu, 17 Aug 2017 14:52:56 +0200 eberlm Replaced subseq with strict_mono
Thu, 22 Jun 2017 10:50:18 +0200 eberlm Contravariant map on filters
Wed, 26 Apr 2017 15:53:35 +0100 paulson Further new material. The simprule status of some exp and ln identities was reverted.
Fri, 10 Mar 2017 23:16:40 +0100 immler modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
Tue, 21 Feb 2017 15:04:01 +0000 paulson Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
Tue, 31 Jan 2017 15:52:47 +0100 eberlm Simplified Gamma_Function
Mon, 09 Jan 2017 14:00:13 +0000 paulson Advanced topology
Wed, 04 Jan 2017 16:18:50 +0000 paulson Many new theorems, and more tidying
Tue, 03 Jan 2017 16:48:49 +0000 paulson A few new lemmas and needed adaptations
Tue, 25 Oct 2016 15:46:07 +0100 paulson more new material
Tue, 18 Oct 2016 12:01:54 +0200 hoelzl HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
Thu, 13 Oct 2016 18:36:06 +0200 hoelzl HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
Fri, 30 Sep 2016 16:08:38 +0200 hoelzl HOL-Probability: more about probability, prepare for Markov processes in the AFP
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Wed, 17 Aug 2016 16:16:38 +0200 eberlm Tuned L'Hospital
Fri, 15 Jul 2016 11:26:36 +0200 wenzelm proper latex;
Fri, 15 Jul 2016 11:07:51 +0200 wenzelm misc tuning and modernization;
Wed, 15 Jun 2016 22:19:03 +0200 hoelzl move open_Collect_eq/less to HOL
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Tue, 14 Jun 2016 15:34:21 +0100 paulson new results about topology
Mon, 13 Jun 2016 15:23:12 +0200 eberlm Facts about HK integration, complex powers, Gamma function
Fri, 27 May 2016 23:35:13 +0200 wenzelm tuned proofs;
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 18 Apr 2016 14:30:32 +0100 paulson new theorems about convex hulls, etc.; also, renamed some theorems
Mon, 04 Apr 2016 16:52:56 +0100 paulson Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
Mon, 07 Mar 2016 14:34:45 +0000 paulson new material to Blochj's theorem, as well as supporting lemmas
Wed, 24 Feb 2016 15:51:01 +0000 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
Tue, 23 Feb 2016 15:47:39 +0000 paulson New and revised material for (multivariate) analysis
Tue, 09 Feb 2016 06:39:31 +0100 hoelzl instantiate topologies for nat, int and enat
Mon, 08 Feb 2016 17:18:13 +0100 hoelzl move product topology to HOL-Complex_Main
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Fri, 22 Jan 2016 16:00:03 +0000 paulson Reorganised a huge proof
less more (0) -100 -60 tip