src/HOL/Analysis/Further_Topology.thy
12 months ago Angeliki KoutsoukouArgyraki 2018-08-28 tagged 21 theories in the Analysis library for the manual
14 months ago paulson 2018-07-15 more de-applying and a fix
15 months ago paulson 2018-06-26 Rationalisation of complex transcendentals, esp the Arg function
16 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
17 months ago nipkow 2018-04-09 removed dots at the end of (sub)titles
20 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
23 months ago paulson 2017-10-31 A few more topological results. And made some slow proofs faster
23 months ago paulson 2017-10-30 More topological results overlooked last time
23 months ago paulson 2017-10-30 New results in topology, mostly from HOL Light's moretop.ml
23 months ago paulson 2017-10-19 Switching to inverse image and constant_on, plus some new material
23 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