src/HOL/Analysis/Inner_Product.thy
3 months ago immler 2019-01-16 bundle syntax for inner
3 months ago nipkow 2019-01-06 typed definitions
3 months ago wenzelm 2019-01-05 isabelle update -u control_cartouches;
3 months ago immler 2018-12-27 moved lemmas up
6 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
9 months ago nipkow 2018-07-13 correct import
9 months ago nipkow 2018-07-12 more economic tagging
9 months ago paulson 2018-07-10 de-applying, etc.
9 months ago paulson 2018-06-26 Rationalisation of complex transcendentals, esp the Arg function
11 months ago immler 2018-05-03 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
11 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
12 months ago paulson 2018-04-15 quite a few more results about negligibility, etc., and a bit of tidying up
12 months ago immler 2018-04-06 a first shot at tagging for HOL-Analysis manual
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
20 months ago Manuel Eberl 2017-08-22 Lemmas about analysis and permutations
2017-04-19 wenzelm 2017-04-19 tuned imports;
2017-02-28 paulson 2017-02-28 Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library