20 months ago |
paulson |
Importation of additional lemmas from metric.ml
|
file |
diff |
annotate
|
2022-02-15 |
paulson |
an assortment of new or stronger lemmas
|
file |
diff |
annotate
|
2019-11-29 |
nipkow |
reduced imports; deleted unusewd minor lemmas for that purpose
|
file |
diff |
annotate
|
2019-11-28 |
nipkow |
tuned
|
file |
diff |
annotate
|
2019-11-28 |
nipkow |
reduced imports
|
file |
diff |
annotate
|
2019-11-04 |
immler |
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
|
file |
diff |
annotate
|
2019-10-09 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
2019-04-12 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
2019-04-10 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
2019-01-23 |
Angeliki KoutsoukouArgyraki |
tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space
|
file |
diff |
annotate
|
2019-01-18 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
2019-01-18 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
2019-01-17 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
2019-01-17 |
Angeliki KoutsoukouArgyraki |
more tagging
|
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 |
nipkow |
Reorg of material
|
file |
diff |
annotate
|
2019-01-16 |
nipkow |
redundant lemma
|
file |
diff |
annotate
|
2019-01-16 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
2019-01-16 |
nipkow |
Reorg of material
|
file |
diff |
annotate
|
2019-01-16 |
nipkow |
tuned headers
|
file |
diff |
annotate
|
2019-01-15 |
nipkow |
moved and renamed class
|
file |
diff |
annotate
|
2019-01-05 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
2018-12-27 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
2018-11-08 |
wenzelm |
isabelle update_cartouches -t;
|
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-03 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
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-05-01 |
paulson |
simplified some messy proofs
|
file |
diff |
annotate
|
2018-04-28 |
paulson |
getting rid of more "defer", etc.
|
file |
diff |
annotate
|
2018-04-27 |
paulson |
minor typeclass generalisations and junk removal
|
file |
diff |
annotate
|
2018-04-26 |
paulson |
small typeclass generalisations
|
file |
diff |
annotate
|
2018-04-26 |
paulson |
some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous
|
file |
diff |
annotate
|
2018-04-25 |
paulson |
more messy proofs redone, and new material
|
file |
diff |
annotate
|
2018-04-25 |
paulson |
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
|
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-15 |
paulson |
various new results on measures, integrals, etc., and some simplified proofs
|
file |
diff |
annotate
|
2018-04-14 |
paulson |
more new theorems on real^1, matrices, etc.
|
file |
diff |
annotate
|
2018-04-14 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
2018-04-09 |
paulson |
merged
|
file |
diff |
annotate
|
2018-04-09 |
paulson |
Syntax for the special cases Min(A`I) and Max (A`I)
|
file |
diff |
annotate
|
2018-04-09 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
2018-04-06 |
immler |
a first shot at tagging for HOL-Analysis manual
|
file |
diff |
annotate
|
2018-02-28 |
wenzelm |
clarified use of vec type syntax;
|
file |
diff |
annotate
|
2018-02-26 |
immler |
generalized
|
file |
diff |
annotate
|
2018-02-25 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
file |
diff |
annotate
|
2018-02-22 |
immler |
merged
|
file |
diff |
annotate
|
2018-02-22 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
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-12-07 |
nipkow |
canonical name
|
file |
diff |
annotate
|
2017-10-08 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
2017-08-17 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
2016-10-17 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
2016-09-27 |
paulson |
a few new theorems and a renaming
|
file |
diff |
annotate
|
2016-09-22 |
paulson |
More mainly topological results
|
file |
diff |
annotate
|