Activity for Robert Himmelmann
-
Robert Himmelmann committed [1ba01c]
Changed prioriy of vector_scalar_mult
-
Added Convex_Euclidean_Space.thy
-
merged
-
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
-
corrected problem in Determinants
-
Corrected definition of is_interval
-
Moved some lemmas about intervals to Topology
-
Removed Convex_Euclidean_Space.thy from Library.
-
removed duplicate lemmas
-
distinguished session for multivariate analysis
-
Made finite cartesian products finite
-
Removed explicit type annotations
-
Added integration to Multivariate-Analysis (upto FTC)
-
Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
-
Support for one-dimensional integration in Multivariate-Analysis
-
the ordering on real^1 is linear
-
replaced \<bullet> with inner
-
tuned
-
added lemmas
-
reset smt_certificates
-
Translated remaining theorems about integration from HOL light.
1
