Thu, 21 Mar 2024 14:19:39 +0000 |
paulson |
New material from a variety of sources (including AFP)
|
file |
diff |
annotate
|
Mon, 19 Feb 2024 14:12:20 +0000 |
paulson |
A small collection of new and useful facts, including the AM-GM inequality
|
file |
diff |
annotate
|
Wed, 07 Feb 2024 11:52:34 +0000 |
paulson |
Further lemmas concerning complexity and measures
|
file |
diff |
annotate
|
Tue, 06 Feb 2024 15:29:10 +0000 |
paulson |
Correct the definition of a convex function, and updated the proofs
|
file |
diff |
annotate
|
Fri, 26 Jan 2024 11:19:22 +0000 |
paulson |
Type class patch suggested by Achim Brucker, plus tidied lemma
|
file |
diff |
annotate
|
Sat, 09 Sep 2023 19:26:08 +0100 |
paulson |
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
|
file |
diff |
annotate
|
Thu, 03 Aug 2023 19:10:36 +0200 |
paulson |
More cosmetic changes
|
file |
diff |
annotate
|
Thu, 02 Mar 2023 17:17:18 +0000 |
paulson |
Some new lemmas. Some tidying up
|
file |
diff |
annotate
|
Sun, 07 Nov 2021 22:14:40 +0000 |
paulson |
new lemmas about convex, concave functions, + tidying
|
file |
diff |
annotate
|
Tue, 06 Oct 2020 20:34:29 +0100 |
paulson |
Simplified some proofs
|
file |
diff |
annotate
|
Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
Thu, 05 Dec 2019 21:03:06 +0100 |
nipkow |
separated Affine theory from Convex
|
file |
diff |
annotate
|
Thu, 05 Dec 2019 18:26:11 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Fri, 15 Nov 2019 16:44:09 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Tue, 05 Nov 2019 21:07:03 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Tue, 05 Nov 2019 19:13:47 +0100 |
nipkow |
removed redundant lemma
|
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 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
Mon, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
Wed, 13 Feb 2019 09:50:16 +0100 |
nipkow |
removed subsumed lemma
|
file |
diff |
annotate
|
Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
Wed, 16 Jan 2019 18:14:02 -0500 |
immler |
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
|
file |
diff |
annotate
|
Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
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
|