src/HOL/Integ/Bin.ML
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
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-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
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-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2000-12-19 paulson 2000-12-19 coping with the re-orientation of #nn=x
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-13 paulson 2000-09-13 more integer theorems, better simplification
2000-08-17 paulson 2000-08-17 better rules for cancellation of common factors across comparisons
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-07-01 nipkow 2000-07-01 Defined abs on int.
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-14 paulson 2000-06-14 new default simprules for m*n = 0
2000-05-04 paulson 2000-05-04 further tidying of integer simprocs
2000-05-03 paulson 2000-05-03 Installation of CombineNumerals for the integers Many bug fixes Removal of AssocFold for addition (nat and int)
2000-04-23 paulson 2000-04-23 removed some duplication, etc.
2000-03-22 paulson 2000-03-22 tidied using new "inst" rule
1999-10-04 wenzelm 1999-10-04 arithmetic now in IntArith;
1999-09-23 nipkow 1999-09-23 Restructured lin.arith.package.
1999-09-21 nipkow 1999-09-21 Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
1999-09-08 paulson 1999-09-08 generalized the theorem bin_add_BIT_Min to bin_add_Min_right
1999-07-23 paulson 1999-07-23 zadd_ac and zmult_ac are no longer included by default
1999-07-19 paulson 1999-07-19 removal of rewrites for Suc(Suc(Suc...)))
1999-07-15 paulson 1999-07-15 qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
1999-07-14 paulson 1999-07-14 new constant folding rewrites
1999-07-13 paulson 1999-07-13 new theorem zmult_eq_0_iff
1999-07-12 paulson 1999-07-12 new theorems for the "at most" relation
1999-07-09 paulson 1999-07-09 products of signs as equivalences
1999-07-08 paulson 1999-07-08 Introduction of integer division algorithm Renaming of theorems from _nat0 to _int0 and _nat1 to _int1
1999-07-06 wenzelm 1999-07-06 use generic numeral encoding and syntax;
1999-06-23 paulson 1999-06-23 rewrite rules to distribute CONSTANT multiplication over sum and difference; removed automatic rewriting of 2x to x+x
1999-05-24 paulson 1999-05-24 Better simplification of (nat #0), (int (Suc 0)), etc
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-03 paulson 1999-03-03 expandshort
1999-01-27 nipkow 1999-01-27 arith_tac for min/max
1999-01-14 nipkow 1999-01-14 More arith refinements.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1999-01-12 nipkow 1999-01-12 Restructured Arithmatic
1999-01-11 nipkow 1999-01-11 More arith simplifications.
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1999-01-05 nipkow 1999-01-05 Instantiated lin.arith.
1998-12-28 paulson 1998-12-28 fixed comments
1998-10-30 paulson 1998-10-30 Explicit (and improved) simprules for binary arithmetic. New default simprules to eliminate (int 0) and (z + - w)
1998-10-23 paulson 1998-10-23 Now users will never see (int 0)
1998-10-01 paulson 1998-10-01 better handling of literals
1998-09-29 paulson 1998-09-29 many renamings and changes. Simproc for cancelling common terms in relations
1998-09-25 paulson 1998-09-25 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-24 paulson 1998-09-24 renamed some axioms; some new theorems
1998-09-23 paulson 1998-09-23 much renaming and reorganization
1998-09-21 paulson 1998-09-21 much renaming and tidying
1998-09-18 paulson 1998-09-18 improved (but still flawed) treatment of binary arithmetic
1998-09-15 paulson 1998-09-15 revised treatment of integers
1998-07-31 paulson 1998-07-31 tidied
1998-07-24 wenzelm 1998-07-24 added ex/MonoidGroups (record example); moved Bin and String examples to ex;
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;