Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
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 21:32:36 +0100 |
immler |
moved lemmas up
|
file |
diff |
annotate
|
Thu, 27 Dec 2018 21:00:50 +0100 |
immler |
generalized to big sum
|
file |
diff |
annotate
|
Mon, 03 Sep 2018 22:38:23 +0200 |
nipkow |
tuned
|
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
|
Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
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
|
Mon, 30 Apr 2018 22:13:04 +0100 |
paulson |
more general 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
|
Fri, 06 Apr 2018 17:34:50 +0200 |
immler |
a first shot at tagging for HOL-Analysis manual
|
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
|
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
|
Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
Fri, 08 Sep 2017 12:49:40 +0100 |
paulson |
Simplicial complexes and triangulations; Baire Category Theorem
|
file |
diff |
annotate
|
Thu, 24 Aug 2017 17:15:53 +0100 |
paulson |
more elimination of "guess", etc.
|
file |
diff |
annotate
|
Tue, 22 Aug 2017 21:36:48 +0200 |
Manuel Eberl |
Lemmas about analysis and permutations
|
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
|
Mon, 14 Aug 2017 18:54:25 +0100 |
paulson |
further Hensock tidy-up
|
file |
diff |
annotate
|
Thu, 27 Jul 2017 15:22:35 +0100 |
paulson |
polytopes: simplical subdivisions, etc.
|
file |
diff |
annotate
|
Wed, 19 Jul 2017 16:41:26 +0100 |
paulson |
new material: Colinearity, convex sets, polytopes
|
file |
diff |
annotate
|
Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
Mon, 10 Oct 2016 15:45:41 +0100 |
paulson |
invariance of domain
|
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
|
Thu, 15 Sep 2016 15:48:37 +0100 |
paulson |
lots of new results about topology, affine dimension etc
|
file |
diff |
annotate
|
Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|