src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
Mon, 14 Mar 2016 15:58:02 +0000 paulson New results about paths, segments, etc. The notion of simply_connected.
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 28 Dec 2015 01:28:28 +0100 wenzelm more symbols;
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Wed, 10 Jun 2015 19:10:20 +0200 wenzelm isabelle update_cartouches;
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Tue, 18 Mar 2014 10:12:58 +0100 immler additional lemmas
Tue, 18 Mar 2014 10:12:58 +0100 immler removed dependencies on theory Ordered_Euclidean_Space
Tue, 18 Mar 2014 10:12:57 +0100 immler use cbox to relax class constraints
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Wed, 12 Feb 2014 08:35:56 +0100 blanchet adapted theories to '{case,rec}_{list,option}' names
Mon, 16 Dec 2013 17:08:22 +0100 immler additional lemmas
Mon, 16 Dec 2013 17:08:22 +0100 immler summarized notions related to ordered_euclidean_space and intervals in separate theory
less more (0) tip