| Tue, 22 Jan 2019 10:50:35 +0000 |
paulson |
some renamings and a bit of new material
|
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
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 18:53:19 +0100 |
nipkow |
tuned headers etc, added bib-file
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:00:50 +0100 |
immler |
generalized to big sum
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
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, 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 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
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
|
| Mon, 30 Apr 2018 22:13:04 +0100 |
paulson |
more general tidying up
|
file |
diff |
annotate
|
| Fri, 27 Apr 2018 20:59:34 +0100 |
paulson |
another big cleanup
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 22:47:04 +0100 |
paulson |
more messy proofs
|
file |
diff |
annotate
|
| Wed, 25 Apr 2018 21:29:02 +0100 |
paulson |
more messy proofs redone, and new material
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 22:22:08 +0100 |
paulson |
fixing more messy proofs
|
file |
diff |
annotate
|
| Mon, 23 Apr 2018 21:57:15 +0100 |
paulson |
tidied some horrid proofs
|
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
|
| 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
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
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
|
| Tue, 05 Dec 2017 12:14:36 +0100 |
Manuel Eberl |
Moved material from AFP to Analysis/Number_Theory
|
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 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Fri, 08 Sep 2017 12:49:40 +0100 |
paulson |
Simplicial complexes and triangulations; Baire Category Theorem
|
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, 20 Jul 2017 14:05:29 +0100 |
paulson |
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
|
file |
diff |
annotate
|
| Wed, 19 Jul 2017 16:41:26 +0100 |
paulson |
new material: Colinearity, convex sets, polytopes
|
file |
diff |
annotate
|
| Thu, 04 May 2017 15:14:49 +0100 |
paulson |
A few more new lemmas
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 17:17:26 +0000 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
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 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
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, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 15:55:53 +0100 |
paulson |
more from moretop.ml
|
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
|
| Mon, 03 Oct 2016 13:01:01 +0100 |
paulson |
new theorems including the theory FurtherTopology
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 15:35:37 +0200 |
hoelzl |
HOL-Analysis: move Product_Vector and Inner_Product from Library
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 12:00:17 +0200 |
hoelzl |
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
|
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
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|