src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
Fri, 25 Sep 2015 16:54:31 +0200 hoelzl prove Liminf_inverse_ereal
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Thu, 23 Jul 2015 16:39:10 +0200 hoelzl reorganized Extended_Real
Wed, 10 Jun 2015 19:10:20 +0200 wenzelm isabelle update_cartouches;
Tue, 27 Jan 2015 16:12:40 +0100 hoelzl ereal: tuned proofs concerning continuity and suprema
Thu, 22 Jan 2015 14:51:08 +0100 hoelzl import general thms from Density_Compiler
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:09:04 +0100 wenzelm modernized header;
Tue, 05 Aug 2014 16:58:19 +0200 wenzelm tuned proofs -- fewer warnings;
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
Mon, 30 Jun 2014 15:45:03 +0200 hoelzl some lemmas about the indicator function; removed lemma sums_def2
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Sun, 16 Feb 2014 21:09:47 +0100 wenzelm tuned proofs;
Tue, 05 Nov 2013 09:44:59 +0100 hoelzl use INF and SUP on conditionally complete lattices in multivariate analysis
Tue, 05 Nov 2013 09:44:58 +0100 hoelzl use bdd_above and bdd_below for conditionally complete lattices
Tue, 05 Nov 2013 09:44:57 +0100 hoelzl generalize SUP and INF to the syntactic type classes Sup and Inf
Sun, 22 Sep 2013 21:04:53 +0200 wenzelm tuned proofs;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:21:00 +0100 hoelzl rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Tue, 05 Mar 2013 15:43:22 +0100 hoelzl generalized lemmas in Extended_Real_Limits
Tue, 05 Mar 2013 15:43:08 +0100 hoelzl move Liminf / Limsup lemmas on complete_lattices to its own file
Wed, 20 Feb 2013 12:04:42 +0100 hoelzl split dense into inner_dense_order and no_top/no_bot
Thu, 31 Jan 2013 11:31:30 +0100 hoelzl use order topology for extended reals
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Sat, 29 Sep 2012 21:59:08 +0200 wenzelm tuned proofs;
Wed, 25 Apr 2012 19:26:00 +0200 hoelzl moved lemmas to appropriate places
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Tue, 20 Sep 2011 11:02:41 -0700 huffman Extended_Real_Limits: generalize some lemmas
Tue, 20 Sep 2011 10:52:08 -0700 huffman add lemmas within_empty and tendsto_bot;
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Tue, 13 Sep 2011 16:21:48 +0200 noschinl tune simpset for Complete_Lattices
Sun, 28 Aug 2011 20:56:49 -0700 huffman move class perfect_space into RealVector.thy;
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Thu, 11 Aug 2011 14:24:05 -0700 huffman avoid duplicate rule warnings
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Tue, 09 Aug 2011 10:30:00 -0700 huffman mark some redundant theorems as legacy
Tue, 19 Jul 2011 14:38:29 +0200 hoelzl add ereal to typeclass infinity
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Mon, 23 May 2011 19:21:05 +0200 hoelzl move lemmas to Extended_Reals and Extended_Real_Limits
Mon, 14 Mar 2011 16:59:37 +0100 wenzelm standardized headers;
Mon, 14 Mar 2011 14:37:49 +0100 hoelzl reworked Probability theory: measures are not type restricted to positive extended reals
Mon, 14 Mar 2011 14:37:47 +0100 hoelzl split Extended_Reals into parts for Library and Multivariate_Analysis
less more (0) tip