src/HOL/Orderings.thy
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
Wed, 10 Oct 2012 12:52:24 +0200 haftmann more explicit code equations
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Sat, 17 Mar 2012 09:51:18 +0100 wenzelm 'definition' no longer exports the foundational "raw_def";
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset
Sun, 26 Feb 2012 20:10:14 +0100 haftmann tuned syntax declarations; tuned structure
Sun, 26 Feb 2012 15:28:48 +0100 haftmann marked candidates for rule declarations
Thu, 23 Feb 2012 20:33:35 +0100 haftmann moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
Sun, 19 Feb 2012 15:30:35 +0100 haftmann distributed lattice properties of predicates to places of instantiation
Mon, 19 Dec 2011 14:41:08 +0100 noschinl weaken preconditions on lemmas
Thu, 15 Dec 2011 16:10:44 +0100 noschinl add complementary lemmas for {min,max}_least
Mon, 24 Oct 2011 16:47:24 +0200 huffman instance bool :: linorder
Mon, 24 Oct 2011 12:26:05 +0200 bulwahn removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
Fri, 21 Oct 2011 11:17:14 +0200 bulwahn replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
Thu, 20 Oct 2011 22:26:02 +0200 blanchet mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Wed, 03 Aug 2011 23:21:52 +0200 haftmann tuned
Sat, 16 Jul 2011 22:04:02 +0200 haftmann consolidated bot and top classes, tuned notation
Wed, 13 Jul 2011 23:49:56 +0200 haftmann uniqueness lemmas for bot and top
Wed, 13 Jul 2011 19:43:12 +0200 haftmann moved lemmas bot_less and less_top to classes bot and top respectively
Wed, 13 Jul 2011 19:40:18 +0200 haftmann tightened specification of classes bot and top: uniqueness of top and bot elements
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
less more (0) -100 -60 tip