| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
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
|
| Mon, 16 Sep 2019 17:03:13 +0100 |
paulson |
A little-known material, and some tidying up
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 14:51:45 +0100 |
paulson |
new material on Analysis, plus some rearrangements
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
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
|
| Wed, 16 Jan 2019 16:50:35 -0500 |
immler |
bundle syntax for inner
|
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
|
| Sun, 06 Jan 2019 12:32:01 +0100 |
nipkow |
typed definitions
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 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
|