src/HOL/Analysis/Further_Topology.thy
4 weeks ago paulson 2019-03-19 new material about topology, etc.; also fixes for yesterday's
2 months ago nipkow 2019-01-28 more canonical and less specialized syntax
2 months ago Angeliki KoutsoukouArgyraki 2019-01-22 minor tagging updates in 13 theories
2 months ago paulson 2019-01-22 renamings and new material
3 months ago immler 2019-01-17 subsection is always %important
3 months ago immler 2019-01-17 redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
3 months ago immler 2019-01-17 revert to 56acd449da41
3 months ago Angeliki KoutsoukouArgyraki 2019-01-17 more tagging
3 months ago haftmann 2019-01-14 tuned proofs
3 months ago immler 2019-01-07 split off Convex.thy: material that does not require Topology_Euclidean_Space
3 months ago wenzelm 2019-01-01 more antiquotations -- less LaTeX macros;
3 months ago nipkow 2018-12-27 tuned headers; ~ -> \<not>
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.
7 months ago Angeliki KoutsoukouArgyraki 2018-08-28 tagged 21 theories in the Analysis library for the manual
9 months ago paulson 2018-07-15 more de-applying and a fix
9 months ago paulson 2018-06-26 Rationalisation of complex transcendentals, esp the Arg function
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 nipkow 2018-04-09 removed dots at the end of (sub)titles
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
17 months ago paulson 2017-10-31 A few more topological results. And made some slow proofs faster
17 months ago paulson 2017-10-30 More topological results overlooked last time
17 months ago paulson 2017-10-30 New results in topology, mostly from HOL Light's moretop.ml
18 months ago paulson 2017-10-19 Switching to inverse image and constant_on, plus some new material
18 months ago paulson 2017-10-10 Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
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
2017-02-21 paulson 2017-02-21 some new material, also recasting some theorems using “obtains”
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2017-01-09 paulson 2017-01-09 fixed LaTeX problems
2017-01-09 paulson 2017-01-09 Jordan Curve Theorem
2017-01-09 paulson 2017-01-09 Advanced topology
2017-01-05 paulson 2017-01-05 facts about ANRs, ENRs, covering spaces
2017-01-05 paulson 2017-01-05 New theory of arcwise connected sets and other new material
2017-01-05 paulson 2017-01-05 connectedness, circles not simply connected , punctured universe
2016-11-19 wenzelm 2016-11-19 more symbols;
2016-10-26 paulson 2016-10-26 Deleted spurious markup
2016-10-25 paulson 2016-10-25 more new material
2016-10-25 paulson 2016-10-25 more new material
2016-10-18 paulson 2016-10-18 Inserted necessary dependency
2016-10-18 hoelzl 2016-10-18 HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp