Wed, 27 Mar 2024 15:16:09 +0000 |
paulson |
New material and a bit of refactoring
|
file |
diff |
annotate
|
Thu, 02 Mar 2023 17:17:18 +0000 |
paulson |
Some new lemmas. Some tidying up
|
file |
diff |
annotate
|
Sun, 01 Jan 2023 00:45:55 +0000 |
paulson |
Big simplifications of old proofs
|
file |
diff |
annotate
|
Fri, 30 Dec 2022 23:21:37 +0000 |
paulson |
Continued proof simplifications
|
file |
diff |
annotate
|
Tue, 24 May 2022 16:21:49 +0100 |
paulson |
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
|
file |
diff |
annotate
|
Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
Sun, 08 Dec 2019 17:42:53 +0100 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Tue, 05 Nov 2019 14:57:41 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Tue, 05 Nov 2019 12:00:23 +0000 |
paulson |
Merge and get rid of closed_segmentI
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 17:06:18 +0000 |
paulson |
Moved or deleted some out of place material, also eliminating obsolete naming conventions
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 17:18:25 -0500 |
immler |
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
|
file |
diff |
annotate
|
Sun, 27 Oct 2019 17:26:50 +0100 |
immler |
example applications of the 'metric' decision procedure, by Maximilian Schäffeler
|
file |
diff |
annotate
|
Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
file |
diff |
annotate
|
Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
Mon, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
Tue, 29 Jan 2019 16:13:11 +0100 |
nipkow |
moved generalized material
|
file |
diff |
annotate
|
Fri, 25 Jan 2019 14:19:19 -0500 |
immler |
generalized
|
file |
diff |
annotate
|
Fri, 25 Jan 2019 13:19:16 +0100 |
nipkow |
moved retracts
|
file |
diff |
annotate
|
Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 14:06:54 +0100 |
immler |
split off Convex.thy: material that does not require Topology_Euclidean_Space
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 13:33:29 +0100 |
immler |
moved setdist to more appropriate places
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 13:16:33 +0100 |
immler |
reduced dependencies of Connected.thy
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 12:31:08 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 11:29:34 +0100 |
immler |
moved material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
Sun, 06 Jan 2019 17:54:49 +0100 |
immler |
moved some material from Connected.thy to more appropriate places
|
file |
diff |
annotate
|
Sat, 29 Dec 2018 20:32:09 +0100 |
immler |
split off theorems involving classes below metric_space and real_normed_vector
|
file |
diff |
annotate
|
Thu, 27 Dec 2018 23:38:55 +0100 |
immler |
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
|
file |
diff |
annotate
|
Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
Wed, 17 Oct 2018 14:19:07 +0100 |
paulson |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
file |
diff |
annotate
|
Fri, 21 Sep 2018 20:47:34 +0100 |
paulson |
more on product (function) topologies
|
file |
diff |
annotate
|
Sun, 16 Sep 2018 14:13:08 +0100 |
paulson |
more lemmas
|
file |
diff |
annotate
|
Thu, 12 Jul 2018 11:23:46 +0200 |
nipkow |
more economic tagging
|
file |
diff |
annotate
|
Tue, 10 Jul 2018 09:38:35 +0200 |
immler |
make theorem, corollary, and proposition %important for HOL-Analysis manual
|
file |
diff |
annotate
|
Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
Tue, 15 May 2018 11:33:43 +0200 |
immler |
move FuncSet back to HOL-Library (amending 493b818e8e10)
|
file |
diff |
annotate
|
Tue, 08 May 2018 10:32:07 +0100 |
paulson |
tidying more messy proofs
|
file |
diff |
annotate
|
Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
Sun, 15 Apr 2018 17:22:47 +0100 |
paulson |
a few more results
|
file |
diff |
annotate
|
Sat, 14 Apr 2018 09:23:00 +0100 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
Fri, 06 Apr 2018 17:34:50 +0200 |
immler |
a first shot at tagging for HOL-Analysis manual
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Thu, 22 Feb 2018 18:01:08 +0100 |
immler |
merged
|
file |
diff |
annotate
|
Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
Wed, 21 Feb 2018 12:57:49 +0000 |
paulson |
Lots of new material about matrices, etc.
|
file |
diff |
annotate
|
Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
Thu, 07 Dec 2017 15:48:50 +0100 |
nipkow |
canonical name
|
file |
diff |
annotate
|
Mon, 30 Oct 2017 16:02:59 +0000 |
paulson |
New results in topology, mostly from HOL Light's moretop.ml
|
file |
diff |
annotate
|
Thu, 19 Oct 2017 17:16:01 +0100 |
paulson |
Switching to inverse image and constant_on, plus some new material
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Mon, 09 Oct 2017 16:14:18 +0100 |
paulson |
Fixed the theorem name "closed_imp_fip_compact"
|
file |
diff |
annotate
|
Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
Fri, 08 Sep 2017 15:27:22 +0100 |
paulson |
Correction of typos and a bit of streamlining
|
file |
diff |
annotate
|
Fri, 08 Sep 2017 12:49:40 +0100 |
paulson |
Simplicial complexes and triangulations; Baire Category Theorem
|
file |
diff |
annotate
|
Sun, 20 Aug 2017 18:55:03 +0200 |
Manuel Eberl |
More lemmas for HOL-Analysis
|
file |
diff |
annotate
|
Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
Sun, 13 Aug 2017 19:24:33 +0100 |
paulson |
general rationalisation of Analysis
|
file |
diff |
annotate
|
Tue, 01 Aug 2017 17:33:04 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 18 Jul 2017 11:35:32 +0200 |
eberlm |
poles and residues of the Gamma function
|
file |
diff |
annotate
|
Thu, 22 Jun 2017 16:31:29 +0100 |
paulson |
New theorems and much tidying up of the old ones
|
file |
diff |
annotate
|
Wed, 21 Jun 2017 17:13:55 +0100 |
paulson |
Tidying up integration theory and some new theorems
|
file |
diff |
annotate
|
Mon, 19 Jun 2017 16:07:47 +0100 |
paulson |
New theorems; stronger theorems; tidier theorems. Also some renaming
|
file |
diff |
annotate
|
Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
Thu, 27 Apr 2017 15:59:00 +0100 |
paulson |
New material (and some tidying) purely in the Analysis directory
|
file |
diff |
annotate
|
Wed, 26 Apr 2017 16:58:31 +0100 |
paulson |
Some fixes related to compactE_image
|
file |
diff |
annotate
|
Fri, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
Wed, 22 Feb 2017 12:30:28 +0000 |
paulson |
new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions
|
file |
diff |
annotate
|
Tue, 21 Feb 2017 17:12:10 +0000 |
paulson |
some new material, also recasting some theorems using “obtains”
|
file |
diff |
annotate
|
Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 17 Jan 2017 11:26:21 +0100 |
wenzelm |
more symbols via abbrevs;
|
file |
diff |
annotate
|
Mon, 09 Jan 2017 14:00:13 +0000 |
paulson |
Advanced topology
|
file |
diff |
annotate
|
Thu, 05 Jan 2017 16:37:49 +0000 |
paulson |
facts about ANRs, ENRs, covering spaces
|
file |
diff |
annotate
|
Thu, 05 Jan 2017 14:18:24 +0000 |
paulson |
New material about path connectedness, etc.
|
file |
diff |
annotate
|
Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
file |
diff |
annotate
|
Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
Sun, 04 Dec 2016 21:40:50 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Tue, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
Thu, 20 Oct 2016 18:41:59 +0200 |
hoelzl |
HOL-Probability: move stopping time from AFP/Markov_Models
|
file |
diff |
annotate
|
Tue, 18 Oct 2016 15:55:53 +0100 |
paulson |
more from moretop.ml
|
file |
diff |
annotate
|
Tue, 18 Oct 2016 12:01:54 +0200 |
hoelzl |
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
Mon, 10 Oct 2016 15:45:41 +0100 |
paulson |
invariance of domain
|
file |
diff |
annotate
|
Sun, 02 Oct 2016 12:32:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
Thu, 29 Sep 2016 13:02:43 +0200 |
hoelzl |
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
|
file |
diff |
annotate
|
Thu, 29 Sep 2016 12:58:55 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
Tue, 27 Sep 2016 16:24:53 +0100 |
paulson |
a few new theorems and a renaming
|
file |
diff |
annotate
|
Thu, 22 Sep 2016 15:44:47 +0100 |
paulson |
More mainly topological results
|
file |
diff |
annotate
|
Wed, 21 Sep 2016 16:59:51 +0100 |
paulson |
new material about topological concepts, etc
|
file |
diff |
annotate
|
Thu, 15 Sep 2016 15:48:37 +0100 |
paulson |
lots of new results about topology, affine dimension etc
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|