src/HOL/Integ/NatBin.thy
2002-05-31 nipkow 2002-05-31 Now arith can deal with div/mod arbitrary nat numerals.
2002-05-15 nipkow 2002-05-15 Set up arith to deal with div 2 and mod 2.
2002-03-07 wenzelm 2002-03-07 renamed nat_number_of to nat_number (avoid clash with separate theorem);
2002-02-25 berghofe 2002-02-25 Introduced variants of operators + * ~ constrained to type int (to make SML/NJ happy).
2002-01-23 wenzelm 2002-01-23 tuned; lemmas nat_number_of;
2001-12-10 berghofe 2001-12-10 Added code generator setup.
2001-08-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-08-03 paulson 2000-08-03 introduction of integer exponentiation
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals