src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported Decision_Procs to new datatypes
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Fri, 04 Apr 2014 17:58:25 +0100 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
Wed, 26 Feb 2014 17:12:07 +0100 wenzelm tuned specifications and proofs;
Tue, 25 Feb 2014 23:12:48 +0100 wenzelm tuned specifications and proofs;
Wed, 12 Feb 2014 08:37:28 +0100 blanchet compile
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 29 Nov 2012 14:05:53 +0100 wenzelm more robust syntax that survives collapse of \<^isub> and \<^sub>;
Sun, 11 Nov 2012 19:24:01 +0100 haftmann modernized, simplified and compacted oracle and proof method glue code;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 27 Jul 2012 19:57:23 +0200 wenzelm tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Mon, 14 Nov 2011 19:35:05 +0100 huffman Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
Mon, 08 Aug 2011 09:52:09 -0700 huffman moved division ring stuff from Rings.thy to Fields.thy
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Sun, 15 May 2011 17:45:53 +0200 wenzelm simplified/unified method_setup/attribute_setup;
Sat, 16 Apr 2011 20:49:48 +0200 wenzelm proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Fri, 25 Feb 2011 20:07:48 +0100 nipkow Some cleaning up
Fri, 25 Feb 2011 14:25:41 +0100 nipkow added simp lemma nth_Cons_pos to List
Thu, 24 Feb 2011 20:52:05 +0100 krauss removed unused lemma
Wed, 23 Feb 2011 11:16:56 +0100 krauss eliminated remdps in favor of List.remdups
Wed, 23 Feb 2011 11:15:06 +0100 krauss recdef -> fun
Wed, 23 Feb 2011 10:48:57 +0100 krauss recdef -> fun
Mon, 21 Feb 2011 23:54:53 +0100 wenzelm merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
Mon, 21 Feb 2011 23:14:36 +0100 krauss removed duplicate declarations
Mon, 21 Feb 2011 23:47:19 +0100 wenzelm tuned proofs -- eliminated prems;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 08 Sep 2010 19:21:46 +0200 haftmann modernized primrec
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.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
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