arith.ML

 val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
 
 goalw Nat.thy [less_def] "<m,n> : pred_nat^+ = (m<n)";
 by (rtac refl 1);
 val less_eq = result();
-
-(*
-val div_simps = [div_termination, cut_apply, less_eq];
-val div_ss = nat_ss addsimps div_simps;
-val div_ss = nat_ss addsimps div_simps;
-*)
 
 goal Arith.thy "!!m. m<n ==> m mod n = m";
 by (rtac (mod_def RS wf_less_trans) 1);
 by(asm_simp_tac HOL_ss 1);
 val mod_less = result();