src/HOL/Decision_Procs/Dense_Linear_Order.thy
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;
Thu, 01 Feb 2018 20:29:53 +0100 wenzelm tuned: more standard use of order;
Thu, 01 Feb 2018 17:21:58 +0100 wenzelm tuned;
Thu, 01 Feb 2018 17:15:07 +0100 wenzelm clarified signature;
Wed, 10 Jan 2018 15:21:49 +0100 nipkow Manual updates towards conversion of "op" syntax
Wed, 01 Jun 2016 15:10:27 +0200 wenzelm prefer rat numberals;
Wed, 01 Jun 2016 10:45:35 +0200 wenzelm tuned signature;
Tue, 31 May 2016 21:54:10 +0200 wenzelm ad-hoc overloading for standard operations on type Rat.rat;
Thu, 05 Nov 2015 10:39:59 +0100 wenzelm isabelle update_cartouches -c -t;
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
Wed, 02 Sep 2015 19:53:49 +0200 wenzelm clarified context;
Tue, 01 Sep 2015 17:25:36 +0200 wenzelm tuned -- avoid slightly odd @{cpat};
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Thu, 09 Jul 2015 23:46:21 +0200 wenzelm tuned proofs;
Wed, 24 Jun 2015 23:03:55 +0200 wenzelm tuned proofs -- less digits;
Sat, 20 Jun 2015 22:20:27 +0200 wenzelm tuned proofs;
Sat, 20 Jun 2015 16:31:44 +0200 wenzelm isabelle update_cartouches;
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 02 Mar 2014 22:39:34 +0100 wenzelm more standard module name;
Thu, 27 Feb 2014 21:27:58 +0100 wenzelm tuned whitespace;
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
less more (0) -60 tip