3 months ago 
paulson 
20190318 
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies

file  diff  annotate 
5 months ago 
Angeliki KoutsoukouArgyraki 
20190123 
tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space

file  diff  annotate 
5 months ago 
immler 
20190117 
subsection is always %important

file  diff  annotate 
5 months ago 
Angeliki KoutsoukouArgyraki 
20190117 
merge

file  diff  annotate 
5 months ago 
Angeliki KoutsoukouArgyraki 
20190117 
more tagging

file  diff  annotate 
5 months ago 
Angeliki KoutsoukouArgyraki 
20190116 
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 
5 months ago 
immler 
20190116 
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars

file  diff  annotate 
5 months ago 
nipkow 
20190116 
Reorg of material

file  diff  annotate 
5 months ago 
nipkow 
20190116 
tuned headers

file  diff  annotate 
5 months ago 
nipkow 
20190116 
Reorg of material

file  diff  annotate 
5 months ago 
nipkow 
20190116 
tuned headers

file  diff  annotate 
9 months ago 
nipkow 
20180924 
Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.

file  diff  annotate 
10 months ago 
Angeliki KoutsoukouArgyraki 
20180828 
tagged 21 theories in the Analysis library for the manual

file  diff  annotate 
13 months ago 
wenzelm 
20180515 
tuned headers;

file  diff  annotate 
13 months ago 
immler 
20180503 
fixed HOLAnalysis

file  diff  annotate 
13 months ago 
immler 
20180503 
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)

file  diff  annotate 
14 months ago 
immler 
20180502 
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly

file  diff  annotate 