src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-14 huffman 2011-11-14 Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-02-25 nipkow 2011-02-25 Some cleaning up
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2011-02-24 krauss 2011-02-24 removed unused lemma
2011-02-23 krauss 2011-02-23 eliminated remdps in favor of List.remdups
2011-02-23 krauss 2011-02-23 recdef -> fun
2011-02-23 krauss 2011-02-23 recdef -> fun
2011-02-21 wenzelm 2011-02-21 merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
2011-02-21 krauss 2011-02-21 removed duplicate declarations
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-08-03 wenzelm 2010-08-03 tuned headers -- more precise load path;
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 using code antiquotation
2010-02-08 haftmann 2010-02-08 tuned proof
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-26 wenzelm 2009-10-26 tuned;
2009-10-25 chaieb 2009-10-25 Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)