src/HOL/Integ/nat_bin.ML
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.