| 2019-01-22 |
Angeliki KoutsoukouArgyraki |
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
|
file |
diff |
annotate
|
| 2019-01-17 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| 2019-01-17 |
immler |
revert to 56acd449da41
|
file |
diff |
annotate
|
| 2019-01-17 |
Angeliki KoutsoukouArgyraki |
merge
|
file |
diff |
annotate
|
| 2019-01-16 |
Angeliki KoutsoukouArgyraki |
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
|
file |
diff |
annotate
|
| 2019-01-16 |
immler |
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
|
file |
diff |
annotate
|
| 2018-09-24 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| 2018-08-28 |
Angeliki KoutsoukouArgyraki |
tagged 21 theories in the Analysis library for the manual
|
file |
diff |
annotate
|
| 2018-05-24 |
immler |
generalized Cramer's rule
|
file |
diff |
annotate
|
| 2018-05-10 |
paulson |
tidied some messy proofs
|
file |
diff |
annotate
|
| 2018-05-10 |
paulson |
auto-tidying
|
file |
diff |
annotate
|
| 2018-05-09 |
paulson |
part tidy-up of Determinants
|
file |
diff |
annotate
|
| 2018-05-03 |
immler |
fixed HOL-Analysis
|
file |
diff |
annotate
|
| 2018-05-03 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|
| 2018-05-02 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| 2018-05-02 |
paulson |
tidying up and using real induction methods
|
file |
diff |
annotate
|
| 2018-04-27 |
paulson |
minor typeclass generalisations and junk removal
|
file |
diff |
annotate
|
| 2018-04-16 |
paulson |
some more random results
|
file |
diff |
annotate
|
| 2018-04-15 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
| 2018-04-14 |
paulson |
more new theorems on real^1, matrices, etc.
|
file |
diff |
annotate
|
| 2018-04-09 |
paulson |
merged
|
file |
diff |
annotate
|
| 2018-04-09 |
paulson |
A couple of new results
|
file |
diff |
annotate
|
| 2018-04-09 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| 2018-02-28 |
immler |
generalized lemmas about orthogonal transformation
|
file |
diff |
annotate
|
| 2018-02-21 |
paulson |
Lots of new material about matrices, etc.
|
file |
diff |
annotate
|
| 2018-02-19 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| 2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| 2017-10-08 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
| 2017-08-18 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| 2016-10-17 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|