src/HOL/Analysis/Further_Topology.thy
3 months ago paulson 2019-03-19 new material about topology, etc.; also fixes for yesterday's
4 months ago nipkow 2019-01-28 more canonical and less specialized syntax
4 months ago Angeliki KoutsoukouArgyraki 2019-01-22 minor tagging updates in 13 theories
4 months ago paulson 2019-01-22 renamings and new material
5 months ago immler 2019-01-17 subsection is always %important
5 months ago immler 2019-01-17 redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
5 months ago immler 2019-01-17 revert to 56acd449da41
5 months ago Angeliki KoutsoukouArgyraki 2019-01-17 more tagging
5 months ago haftmann 2019-01-14 tuned proofs
5 months ago immler 2019-01-07 split off Convex.thy: material that does not require Topology_Euclidean_Space
5 months ago wenzelm 2019-01-01 more antiquotations -- less LaTeX macros;
5 months ago nipkow 2018-12-27 tuned headers; ~ -> \<not>
8 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 Angeliki KoutsoukouArgyraki 2018-08-28 tagged 21 theories in the Analysis library for the manual
11 months ago paulson 2018-07-15 more de-applying and a fix
11 months ago paulson 2018-06-26 Rationalisation of complex transcendentals, esp the Arg function
13 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
14 months ago nipkow 2018-04-09 removed dots at the end of (sub)titles
17 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
19 months ago paulson 2017-10-31 A few more topological results. And made some slow proofs faster
19 months ago paulson 2017-10-30 More topological results overlooked last time
19 months ago paulson 2017-10-30 New results in topology, mostly from HOL Light's moretop.ml
20 months ago paulson 2017-10-19 Switching to inverse image and constant_on, plus some new material
20 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