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