src/HOL/Analysis/Homeomorphism.thy
Thu, 03 May 2018 16:17:44 +0200 immler fixed HOL-Analysis
Thu, 03 May 2018 15:07:14 +0200 immler merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
Wed, 02 May 2018 13:49:38 +0200 immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
Wed, 02 May 2018 23:32:47 +0100 paulson tidying up and using real induction methods
Thu, 19 Apr 2018 16:10:06 +0100 paulson tuning of a proof
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Thu, 19 Oct 2017 17:16:01 +0100 paulson Switching to inverse image and constant_on, plus some new material
Tue, 10 Oct 2017 17:15:37 +0100 paulson Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
Fri, 29 Sep 2017 16:55:08 +0100 paulson eliminated a needless dependence on the theorem homeomorphic_punctured_sphere_affine_gen
Mon, 25 Sep 2017 15:49:27 +0100 paulson Tiny presentational improvements to homeomorphic_punctured_sphere_affine_gen
Wed, 19 Jul 2017 16:41:26 +0100 paulson new material: Colinearity, convex sets, polytopes
Tue, 28 Feb 2017 13:51:47 +0000 paulson Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
Thu, 05 Jan 2017 17:10:13 +0000 paulson covering space lift lemmas
Thu, 05 Jan 2017 16:37:49 +0000 paulson facts about ANRs, ENRs, covering spaces
Thu, 05 Jan 2017 15:03:37 +0000 paulson connectedness, circles not simply connected , punctured universe
Wed, 04 Jan 2017 16:18:50 +0000 paulson Many new theorems, and more tidying
Tue, 25 Oct 2016 15:46:07 +0100 paulson more new material
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Tue, 27 Sep 2016 16:24:53 +0100 paulson a few new theorems and a renaming
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Mon, 08 Aug 2016 14:13:14 +0200 hoelzl rename HOL-Multivariate_Analysis to HOL-Analysis.
less more (0) tip