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

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

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

file  diff  annotate 
3 months ago 
Angeliki KoutsoukouArgyraki 
20190117 
merge

file  diff  annotate 
3 months ago 
Angeliki KoutsoukouArgyraki 
20190117 
more tagging

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

file  diff  annotate 
3 months ago 
nipkow 
20190116 
Reorg of material

file  diff  annotate 
3 months ago 
nipkow 
20190116 
tuned headers

file  diff  annotate 
3 months ago 
nipkow 
20190116 
Reorg of material

file  diff  annotate 
3 months ago 
nipkow 
20190116 
tuned headers

file  diff  annotate 
7 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 
7 months ago 
Angeliki KoutsoukouArgyraki 
20180828 
tagged 21 theories in the Analysis library for the manual

file  diff  annotate 
11 months ago 
wenzelm 
20180515 
tuned headers;

file  diff  annotate 
11 months ago 
immler 
20180503 
fixed HOLAnalysis

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

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

file  diff  annotate 