src/HOL/Decision_Procs/Dense_Linear_Order.thy
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Sun, 18 Aug 2013 15:31:12 +0200 wenzelm prefer plain subscript;
Mon, 20 May 2013 20:47:33 +0200 wenzelm proper context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Oct 2012 15:39:01 +0200 wenzelm added some ad-hoc namespace prefixes to avoid duplicate facts;
Fri, 21 Sep 2012 20:54:48 +0200 wenzelm misc tuning;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Mon, 08 Aug 2011 09:52:09 -0700 huffman moved division ring stuff from Rings.thy to Fields.thy
Fri, 25 Feb 2011 20:07:48 +0100 nipkow Some cleaning up
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Tue, 25 May 2010 22:21:31 +0200 wenzelm moved ML files where they are actually used;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Fri, 07 May 2010 16:12:26 +0200 haftmann renamed Normalizer to the more specific Semiring_Normalizer
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"
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Wed, 10 Feb 2010 08:49:26 +0100 haftmann moved constants inverse and divide to Ring.thy
Mon, 08 Feb 2010 14:22:22 +0100 haftmann dropped accidental duplication of "lin" prefix from cs. 108662d50512
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
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Wed, 29 Apr 2009 14:20:26 +0200 haftmann farewell to class recpower
Sun, 05 Apr 2009 19:21:51 +0100 chaieb fixed usage of rational constants
Fri, 27 Mar 2009 10:12:55 +0100 haftmann merged
Fri, 27 Mar 2009 10:05:11 +0100 haftmann normalized imports
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Sun, 22 Mar 2009 20:46:10 +0100 haftmann distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
Mon, 16 Mar 2009 18:24:30 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Wed, 11 Mar 2009 10:58:18 +0100 hoelzl Updated paths in Decision_Procs comments and NEWS
Mon, 09 Feb 2009 16:43:52 +0000 chaieb A generic decision procedure for linear rea arithmetic and normed vector spaces
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
less more (0) tip