src/HOL/Orderings.thy
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;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Wed, 08 Dec 2010 15:05:46 +0100 haftmann bot comes before top, inf before sup etc.
Wed, 08 Dec 2010 14:52:23 +0100 haftmann nice syntax for lattice INFI, SUPR;
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Tue, 24 Aug 2010 14:41:37 +0200 hoelzl moved generic lemmas in Probability to HOL
Mon, 23 Aug 2010 14:21:57 +0200 blanchet "no_atp" fact that leads to unsound proofs in Sledgehammer
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Tue, 04 May 2010 08:55:43 +0200 haftmann locale predicates of classes carry a mandatory "class" prefix
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Thu, 04 Mar 2010 18:42:39 +0100 hoelzl Add dense_le, dense_le_bounded, field_le_mult_one_interval.
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Mon, 22 Feb 2010 15:53:18 +0100 haftmann distributed theory Algebras to theories Groups and Lattices
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Mon, 04 Jan 2010 16:00:23 +0100 haftmann moved name duplicates to end of theory; reduced warning noise
Fri, 11 Dec 2009 14:43:56 +0100 haftmann moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 09 Oct 2009 13:34:34 +0200 haftmann tuned order of lemmas
Wed, 07 Oct 2009 14:01:26 +0200 haftmann added bot_boolE, top_boolI
Sun, 26 Jul 2009 22:28:31 +0200 wenzelm replaced old METAHYPS by FOCUS;
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Wed, 15 Apr 2009 15:52:37 +0200 haftmann code generator bootstrap theory src/Tools/Code_Generator.thy
Mon, 30 Mar 2009 22:48:15 +0200 wenzelm simplified 'print_orders' command;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Fri, 06 Mar 2009 14:33:19 +0100 haftmann added strict_mono predicate
Thu, 26 Feb 2009 16:32:46 +0100 berghofe Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
Wed, 21 Jan 2009 16:47:31 +0100 haftmann dropped ID
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Fri, 24 Oct 2008 17:48:37 +0200 haftmann new classes "top" and "bot"
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 07 Oct 2008 16:07:21 +0200 haftmann tuned min/max code generation
less more (0) -100 -60 tip