| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 21 Mar 2019 14:18:22 +0000 |
paulson |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
file |
diff |
annotate
|
| Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| Wed, 29 Aug 2018 07:50:28 +0100 |
immler |
tagged some theories
|
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
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 28 Oct 2017 23:32:37 +0200 |
immler |
generalized
|
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
|
| 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
|
| Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
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
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|