| Sun, 07 May 2023 14:52:53 +0100 |
paulson |
Importation of additional lemmas from metric.ml
|
file |
diff |
annotate
|
| Tue, 15 Feb 2022 13:00:05 +0000 |
paulson |
an assortment of new or stronger lemmas
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 17:43:00 +0100 |
nipkow |
reduced imports; deleted unusewd minor lemmas for that purpose
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 18:40:39 +0100 |
nipkow |
reduced imports
|
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
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 23 Jan 2019 03:29:34 +0000 |
Angeliki KoutsoukouArgyraki |
tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space
|
file |
diff |
annotate
|
| Fri, 18 Jan 2019 21:22:46 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| Fri, 18 Jan 2019 21:20:14 +0100 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 15:50:28 +0000 |
Angeliki KoutsoukouArgyraki |
more tagging
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 21:27:33 +0000 |
Angeliki KoutsoukouArgyraki |
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 17:03:31 +0100 |
nipkow |
Reorg of material
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 16:18:53 +0100 |
nipkow |
redundant lemma
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 15:53:12 +0100 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 11:48:06 +0100 |
nipkow |
Reorg of material
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 10:27:57 +0100 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
| Tue, 15 Jan 2019 21:31:20 +0100 |
nipkow |
moved and renamed class
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 13:28:39 +0100 |
Angeliki KoutsoukouArgyraki |
tagged 21 theories in the Analysis library for the manual
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
| Thu, 03 May 2018 16:17:44 +0200 |
immler |
fixed HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 03 May 2018 15:07:14 +0200 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
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
|
| Wed, 02 May 2018 23:32:47 +0100 |
paulson |
tidying up and using real induction methods
|
file |
diff |
annotate
|
| Tue, 01 May 2018 23:25:00 +0100 |
paulson |
simplified some messy proofs
|
file |
diff |
annotate
|
| Sat, 28 Apr 2018 21:37:45 +0100 |
paulson |
getting rid of more "defer", etc.
|
file |
diff |
annotate
|
| Fri, 27 Apr 2018 12:38:30 +0100 |
paulson |
minor typeclass generalisations and junk removal
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 16:14:35 +0100 |
paulson |
small typeclass generalisations
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 12:55:48 +0100 |
paulson |
some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
|
file |
diff |
annotate
|
| Wed, 25 Apr 2018 21:29:02 +0100 |
paulson |
more messy proofs redone, and new material
|
file |
diff |
annotate
|
| Wed, 25 Apr 2018 15:36:29 +0100 |
paulson |
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 21:41:40 +0100 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 13:57:00 +0100 |
paulson |
various new results on measures, integrals, etc., and some simplified proofs
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 20:19:52 +0100 |
paulson |
more new theorems on real^1, matrices, etc.
|
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 17:21:10 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 15:20:11 +0100 |
paulson |
Syntax for the special cases Min(A`I) and Max (A`I)
|
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
|
| Wed, 28 Feb 2018 13:37:33 +0100 |
wenzelm |
clarified use of vec type syntax;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 09:58:47 +0100 |
immler |
generalized
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:54:55 +0000 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
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
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
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
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
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
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 13:56:51 +0200 |
hoelzl |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|