src/HOL/Topological_Spaces.thy
Tue, 06 Oct 2015 17:46:07 +0200 wenzelm isabelle update_cartouches;
Fri, 02 Oct 2015 15:07:41 +0100 paulson New theorems about connected sets. And pairwise moved to Set.thy.
Fri, 25 Sep 2015 16:54:31 +0200 hoelzl prove Liminf_inverse_ereal
Tue, 22 Sep 2015 16:55:07 +0100 paulson New lemmas
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
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, 14 Jul 2015 13:37:44 +0200 hoelzl add continuous_onI_mono
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Thu, 07 May 2015 15:34:28 +0200 hoelzl generalized tends over powr; added DERIV rule for powr
Mon, 04 May 2015 17:35:31 +0200 hoelzl rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
Tue, 28 Apr 2015 16:23:38 +0100 paulson New material about complex transcendental functions (especially Ln, Arg) and polynomials
Sun, 12 Apr 2015 11:34:09 +0200 hoelzl move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
Sun, 12 Apr 2015 11:33:19 +0200 hoelzl move filters to their own theory
Wed, 08 Apr 2015 21:42:08 +0200 wenzelm more standard access to goal state;
Wed, 08 Apr 2015 19:58:52 +0200 wenzelm tuned signature;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 27 Jan 2015 16:12:40 +0100 hoelzl ereal: tuned proofs concerning continuity and suprema
Mon, 08 Dec 2014 14:32:11 +0100 hoelzl instance bool and enat as topologies
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 20 Oct 2014 18:33:14 +0200 hoelzl add tendsto_const and tendsto_ident_at as simp and intro rules
Sat, 16 Aug 2014 14:42:35 +0200 wenzelm updated to named_theorems;
Mon, 30 Jun 2014 15:45:25 +0200 hoelzl more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Tue, 13 May 2014 11:35:47 +0200 hoelzl clean up Lebesgue integration
Thu, 10 Apr 2014 17:48:18 +0200 kuncar setup for Transfer and Lifting from BNF; tuned thm names
Thu, 10 Apr 2014 17:48:14 +0200 kuncar left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Mon, 31 Mar 2014 12:16:37 +0200 hoelzl add connected_local_const
Wed, 26 Mar 2014 14:00:37 +0000 paulson Some useful lemmas
Thu, 20 Mar 2014 21:07:57 +0100 wenzelm enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Mon, 10 Mar 2014 20:04:40 +0100 hoelzl introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:14:09 +0100 blanchet renamed 'filter_rel' to 'rel_filter'
Thu, 06 Mar 2014 14:57:14 +0100 blanchet renamed 'set_rel' to 'rel_set'
Thu, 27 Feb 2014 16:07:21 +0000 paulson A bit of tidying up
Tue, 25 Feb 2014 16:17:20 +0000 paulson More complex-related lemmas
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Tue, 18 Feb 2014 23:03:49 +0100 kuncar delete or move now not necessary reflexivity rules due to 1726f46d2aa8
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Wed, 18 Dec 2013 11:53:40 +0100 hoelzl modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
Tue, 05 Nov 2013 09:44:58 +0100 hoelzl use bdd_above and bdd_below for conditionally complete lattices
Fri, 27 Sep 2013 09:26:31 +0200 Andreas Lochbihler add relator for 'a filter and parametricity theorems
Tue, 24 Sep 2013 15:03:49 -0700 huffman factor out new lemma
Tue, 24 Sep 2013 15:03:49 -0700 huffman replace lemma with more general simp rule
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Thu, 30 May 2013 23:29:33 +0200 wenzelm tuned headers;
Thu, 25 Apr 2013 11:59:21 +0200 hoelzl revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
Thu, 25 Apr 2013 10:35:56 +0200 hoelzl renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
Wed, 24 Apr 2013 13:28:30 +0200 hoelzl spell conditional_ly_-complete lattices correct
less more (0) -60 tip