src/HOL/Analysis/Homotopy.thy
Sun, 19 Apr 2020 12:02:26 +0100 paulson the rest of the applys
Sat, 18 Apr 2020 23:13:17 +0100 paulson more applys
Sun, 12 Apr 2020 21:53:58 +0100 paulson more cleaning up Homotopy
Sun, 12 Apr 2020 10:51:51 +0100 paulson cleaning up Homotopy
Tue, 31 Mar 2020 15:51:15 +0200 nipkow cleaned proofs
Wed, 04 Dec 2019 23:11:29 +0100 nipkow moved starlike where it belongs
Thu, 28 Nov 2019 23:06:22 +0100 nipkow tuned
Wed, 09 Oct 2019 14:51:54 +0000 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
Tue, 08 Oct 2019 10:26:40 +0000 haftmann formally augmented corresponding rules for field_simps
Fri, 26 Apr 2019 16:51:40 +0100 paulson Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
Fri, 12 Apr 2019 22:09:25 +0200 wenzelm modernized tags: default scope excludes proof;
Tue, 02 Apr 2019 14:51:27 +0200 wenzelm eliminated hard TABs;
Tue, 26 Mar 2019 17:01:36 +0000 paulson generalised homotopic_with to topologies; homotopic_with_canon is the old version
Tue, 19 Mar 2019 16:14:51 +0000 paulson new material about topology, etc.; also fixes for yesterday's
Mon, 18 Mar 2019 15:35:34 +0000 paulson new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
Thu, 31 Jan 2019 13:08:59 +0000 haftmann proper congruence rule for image operator
Tue, 22 Jan 2019 12:00:16 +0000 paulson renamings and new material
Mon, 07 Jan 2019 14:57:45 +0100 immler split off Homotopy.thy
less more (0) tip