2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-02-16 huffman 2008-02-16 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated, integer);
2007-08-14 nipkow 2007-08-14 extended linear arith capabilities with code by Amine
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-07-31 wenzelm 2007-07-31 tuned LinArith setup;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-06-16 nipkow 2007-06-16 The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant.
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;