src/HOL/Integ/NatBin.ML
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-24 wenzelm 2000-07-24 avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?);
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-14 paulson 2000-06-14 tidied a proof using new lemmas for signs of products
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-12 paulson 2000-05-12 tidying, especially to remove zcompare_rls from proofs
2000-05-05 paulson 2000-05-05 new lemmas about binary division
2000-05-04 paulson 2000-05-04 a safer way of proving literal equalities
2000-05-04 paulson 2000-05-04 new lemmas concerning powers and #mmm
2000-05-02 paulson 2000-05-02 now with combine_numerals
2000-04-21 paulson 2000-04-21 moved the simproc code to NatSimprocs.ML
2000-04-18 paulson 2000-04-18 instantiates new simprocs for numerals of type "nat"
2000-04-13 nipkow 2000-04-13 made mod_less_divisor a simplification rule.
2000-03-22 paulson 2000-03-22 tidied using new "inst" rule
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 nipkow 2000-03-13 exhaust_tac -> cases_tac
2000-02-18 nipkow 2000-02-18 installed lin arith for nat numerals.
2000-01-10 nipkow 2000-01-10 int:nat->int is pushed inwards.
1999-11-24 paulson 1999-11-24 tidied, choosing nicer names
1999-09-28 paulson 1999-09-28 zero_is_mult, by symmetry
1999-09-08 paulson 1999-09-08 simplification of relations involving 0, Suc and natural-number numerals
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1999-07-26 paulson 1999-07-26 expandshort
1999-07-23 paulson 1999-07-23 zmult_ac are no longer included by default
1999-07-21 paulson 1999-07-21 more existing theorems renamed to use #0; also new results
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals