impose hyps on initial goal configuration (prevents res_inst_tac problems);
(* 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