src/HOL/Orderings.thy
Fri, 15 Feb 2019 18:24:22 +0000 haftmann proper installation of ancient procedure for preorders
Mon, 04 Feb 2019 17:19:04 +0100 Manuel Eberl Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Wed, 17 Jan 2018 12:27:06 +0100 nipkow more lemmas by Gouezele
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings;
Thu, 11 Jan 2018 10:13:42 +0100 nipkow line break before op was intentional
Wed, 10 Jan 2018 18:18:34 +0100 nipkow tuned notation
Wed, 10 Jan 2018 15:21:49 +0100 nipkow Manual updates towards conversion of "op" syntax
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Tue, 30 May 2017 10:03:35 +0200 nipkow redefined Greatest
Tue, 03 Jan 2017 16:48:49 +0000 paulson A few new lemmas and needed adaptations
Tue, 18 Oct 2016 15:55:53 +0100 paulson more from moretop.ml
Wed, 07 Sep 2016 11:59:07 +0200 haftmann keep locale lifting rules on the global level
Sat, 11 Jun 2016 16:22:42 +0200 haftmann boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
Fri, 27 May 2016 23:58:24 +0200 wenzelm tuned proofs;
Sat, 05 Mar 2016 19:58:56 +0100 wenzelm old HOL syntax is for input only;
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Thu, 10 Dec 2015 13:38:40 +0000 paulson not_leE -> not_le_imp_less and other tidying
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Wed, 18 Nov 2015 15:23:34 +0000 paulson New theorems mostly from Peter Gammie
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Thu, 16 Apr 2015 15:22:44 +0200 wenzelm discontinued pointless warnings: commands are only defined inside a theory context;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Thu, 10 Apr 2014 12:00:25 +0200 wenzelm modernized simproc_setup;
Thu, 10 Apr 2014 11:24:58 +0200 wenzelm misc tuning;
Mon, 10 Mar 2014 20:04:40 +0100 hoelzl introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Wed, 25 Dec 2013 15:52:25 +0100 haftmann postponed min/max lemmas until abstract lattice is available
Wed, 25 Dec 2013 15:52:25 +0100 haftmann tuned structure of min/max lemmas
Tue, 24 Dec 2013 11:24:16 +0100 haftmann tuning and augmentation of min/max lemmas;
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Tue, 27 Aug 2013 16:06:27 +0200 hoelzl renamed inner_dense_linorder to dense_linorder
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Fri, 29 Mar 2013 22:13:02 +0100 wenzelm tuned message;
Tue, 26 Mar 2013 21:53:56 +0100 haftmann more uniform style for interpretation and sublocale declarations
Sat, 23 Mar 2013 17:11:06 +0100 haftmann locales for abstract orders
Wed, 20 Feb 2013 12:04:42 +0100 hoelzl split dense into inner_dense_order and no_top/no_bot
Sun, 24 Feb 2013 20:29:13 +0100 haftmann turned example into library for comparing growth of functions
less more (0) -100 -60 tip