src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
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
Thu, 19 Aug 2010 16:08:59 +0200 haftmann tuned quotes
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Tue, 03 Aug 2010 16:48:36 +0200 wenzelm tuned headers -- more precise load path;
Tue, 08 Jun 2010 16:37:19 +0200 haftmann qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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 17:12:22 +0100 haftmann using code antiquotation
Mon, 08 Feb 2010 14:06:43 +0100 haftmann tuned proof
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, 12 Nov 2009 17:21:48 +0100 hoelzl New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
Wed, 28 Oct 2009 00:24:38 +0100 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 26 Oct 2009 20:41:26 +0100 wenzelm tuned;
Sun, 25 Oct 2009 08:57:35 +0100 chaieb Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
less more (0) tip