src/HOL/Decision_Procs/MIR.thy
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