src/HOL/ex/BinEx.thy
2009-05-08 haftmann 2009-05-08 explicit method linarith
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2006-10-01 wenzelm 2006-10-01 tuned;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2003-07-22 paulson 2003-07-22 Added some regression testing for simprocs
2003-07-15 paulson 2003-07-15 Fixing a simproc bug
2002-08-12 nipkow 2002-08-12 *** empty log message ***
2002-05-31 paulson 2002-05-31 fixed a proof near the end
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-01-02 paulson 2002-01-02 Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-02-01 wenzelm 2001-02-01 converted to new-style theories;
2000-07-13 wenzelm 2000-07-13 tuned;
1999-07-08 paulson 1999-07-08 Introduction of integer division algorithm
1998-09-24 paulson 1998-09-24 added correctness proofs for arithmetic
1998-07-24 wenzelm 1998-07-24 added ex/MonoidGroups (record example); moved Bin and String examples to ex;