src/HOL/Decision_Procs/MIR.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-25 bulwahn 2012-02-25 removing unnecessary assumptions in RealDef; simplifying proofs in Float, MIR, and Ferrack
2012-01-06 haftmann 2012-01-06 prefer concat over foldl append []
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-03-03 wenzelm 2011-03-03 tuned proofs -- eliminated prems;
2011-03-03 wenzelm 2011-03-03 removed spurious 'unused_thms' (cf. 1a65b780bd56);
2011-02-25 nipkow 2011-02-25 Some cleaning up
2011-02-24 krauss 2011-02-24 recdef -> fun(ction)
2011-02-24 krauss 2011-02-24 eliminated clones of List.upto
2011-02-21 wenzelm 2011-02-21 tuned proofs -- eliminated prems;
2011-01-07 bulwahn 2011-01-07 adopting proofs due to new list comprehension to set comprehension simproc
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
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-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-05-12 haftmann 2010-05-12 tuned test problems
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-28 haftmann 2010-04-28 use code_reflect
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
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-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-20 nipkow 2009-06-20 added lemmas; tuned
2009-06-17 huffman 2009-06-17 new GCD library, courtesy of Jeremy Avigad
2009-03-22 nipkow 2009-03-22 1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
2009-03-11 hoelzl 2009-03-11 Updated paths in Decision_Procs comments and NEWS
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-26 huffman 2009-02-26 add type annotation
2009-02-25 huffman 2009-02-25 generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there