20020531 
nipkow 
20020531 
Now arith can deal with div/mod arbitrary nat numerals.

file  diff  annotate 
20020515 
nipkow 
20020515 
Set up arith to deal with div 2 and mod 2.

file  diff  annotate 
20020307 
wenzelm 
20020307 
renamed nat_number_of to nat_number (avoid clash with separate theorem);

file  diff  annotate 
20020225 
berghofe 
20020225 
Introduced variants of operators + * ~ constrained to type int
(to make SML/NJ happy).

file  diff  annotate 
20020123 
wenzelm 
20020123 
tuned;
lemmas nat_number_of;

file  diff  annotate 
20011210 
berghofe 
20011210 
Added code generator setup.

file  diff  annotate 
20010807 
paulson 
20010807 
Tweaks for 1 > 1'

file  diff  annotate 
20010806 
nipkow 
20010806 
turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.

file  diff  annotate 
20001201 
nipkow 
20001201 
Linear arithmetic now copes with mixed nat/int formulae.

file  diff  annotate 
20000803 
paulson 
20000803 
introduction of integer exponentiation

file  diff  annotate 
19990719 
paulson 
19990719 
NatBin: binary arithmetic for the naturals

file  diff  annotate 