2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-11-29 paulson 2000-11-29 invoking CancelNumeralFactorFun
2000-08-10 paulson 2000-08-10 new structure field "add" for CombineNumerals
2000-08-07 paulson 2000-08-07 added a dummy "thm list" argument to prove_conv for the new interface to Cancel_Numerals
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;