| Thu, 10 May 2018 22:03:51 +0100 |
paulson |
tidied some messy proofs
|
file |
diff |
annotate
|
| Thu, 10 May 2018 15:59:39 +0100 |
paulson |
auto-tidying
|
file |
diff |
annotate
|
| Wed, 09 May 2018 22:11:02 +0100 |
paulson |
part tidy-up of Determinants
|
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
|
| Fri, 27 Apr 2018 12:38:30 +0100 |
paulson |
minor typeclass generalisations and junk removal
|
file |
diff |
annotate
|
| Mon, 16 Apr 2018 21:23:38 +0100 |
paulson |
some more random results
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 21:41:40 +0100 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 20:19:52 +0100 |
paulson |
more new theorems on real^1, matrices, etc.
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 17:21:10 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 17:20:58 +0100 |
paulson |
A couple of new results
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| Wed, 28 Feb 2018 15:53:05 +0100 |
immler |
generalized lemmas about orthogonal transformation
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 12:57:49 +0000 |
paulson |
Lots of new material about matrices, etc.
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
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, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
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
|