Now arith can deal with div/mod arbitrary nat numerals.
(* Title: ZF/ArithSimp.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of CambridgeArithmetic with simplification*)theory ArithSimp = Arithfiles "arith_data.ML":end